reconsider R = id X as Relation of X by Lm4;
take R ; :: thesis: ( R is total & R is reflexive & R is symmetric & R is antisymmetric & R is transitive )
thus ( R is total & R is reflexive & R is symmetric & R is antisymmetric & R is transitive ) by Lm3; :: thesis: verum