let R1, R2 be non empty RelStr ; :: thesis: ( the carrier of R1 = the carrier of R2 & LAp R1 cc= LAp R2 implies the InternalRel of R2 c= the InternalRel of R1 )
assume A1: ( the carrier of R1 = the carrier of R2 & LAp R1 cc= LAp R2 ) ; :: thesis: the InternalRel of R2 c= the InternalRel of R1
( UAp R1 = Flip (LAp R1) & UAp R2 = Flip (LAp R2) ) by ROUGHS_2:28;
hence the InternalRel of R2 c= the InternalRel of R1 by Prop17A, A1, FlipCC; :: thesis: verum