t:Graph. Edges(t) 
Typet:Graph. Incidence(t) Edges(t)
Vertices(t)
Vertices(t)t:Graph. t.o Topt:Graph. Vertices(t) Typee:Type(evv)Top Type{i'} Type| Some definitions of interest. | |
| gr_e | Def Edges(t) == 1of(2of(t)) |
| Thm* t:Graph. Edges(t) Type | |
| gr_f | Def Incidence(t) == 1of(2of(2of(t))) |
| Thm* t:Graph. Incidence(t) Edges(t)Vertices(t)Vertices(t) | |
| gr_o | Def t.o == 2of(2of(2of(t))) |
| Thm* t:Graph. t.o Top | |
| gr_v | Def Vertices(t) == 1of(t) |
| Thm* t:Graph. Vertices(t) Type | |
| graph | Def Graph == v:Typee:Type(evv)Top |
| Thm* Graph Type{i'} | |
| top | Def Top == Void given Void |
| Thm* Top Type |
About:
 |  |  |  |  |  |  |  |  |  |