:: deftheorem defines ~ LATTICE3:def 5 :
for A being RelStr holds A ~ = RelStr(# the carrier of A,( the InternalRel of A ~) #);