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