Metamath Proof Explorer

Syntax definition ccplgr

Description: Extend class notation with (arbitrary) complete graphs.

Ref Expression
Assertion ccplgr 
class ComplGraph