Thms finite sets Sections AutomataTheory Doc

lelt Def i j < k == ij & j < k

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