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