int_seg |
Def {i..j Thm* |
int_upper |
Def {i...} == {j: Thm* |
equiv_rel |
Def compound
EquivRel x,y:T. E(x;y)
== Refl(T;x,y.E(x;y)) & Sym x,y:T. E(x;y) & Trans x,y:T. E(x;y)
Thm* |
lelt |
Def i |
le |
Def A Thm* |
trans |
Def basic
Trans x,y:T. E(x;y) == Thm* |
sym |
Def basic
Sym x,y:T. E(x;y) == Thm* |
refl |
Def basic
Refl(T;x,y.E(x;y)) == Thm* |
not |
Def Thm* ( |