Definitions graph 1 1 Sections Graphs Doc

Some definitions of interest.
ge Def ij == ji
Thm* i,j:. (ij) Prop
gt Def i > j == j < i
Thm* i,j:. (i > j) Prop
int_lower Def {...i} == {j:| ji }
Thm* i:. {...i} Type
int_nzero Def == {i:| i 0 }
Thm* Type
nat Def == {i:| 0i }
Thm* Type
le Def AB == B < A
Thm* i,j:. (ij) Prop
nat_plus Def == {i:| 0 < i }
Thm* Type
not Def A == A False
Thm* A:Prop. (A) Prop

About:
intnatural_numberless_thansetuniversemember
propimpliesfalseall!abstraction

Definitions graph 1 1 Sections Graphs Doc