theorem :: LATTICE3:8

for A being RelStr holds (A ~) ~ = RelStr(# the carrier of A, the InternalRel of A #) ;