let R be RelStr ; :: thesis: the carrier of R = the carrier of (R ~ )
R ~ = RelStr(# the carrier of R,(the InternalRel of R ~ ) #) by LATTICE3:def 5;
hence the carrier of R = the carrier of (R ~ ) ; :: thesis: verum