A ~ = RelStr(# the carrier of A,(the InternalRel of A ~ ) #) ;
hence ( A ~ is reflexive & A ~ is transitive & A ~ is antisymmetric ) ; :: thesis: verum