let R1, R2 be non empty RelStr ; :: thesis: ( the carrier of R1 = the carrier of R2 & LAp R1 = LAp R2 implies the InternalRel of R2 = the InternalRel of R1 )
assume A1: ( the carrier of R1 = the carrier of R2 & LAp R1 = LAp R2 ) ; :: thesis: the InternalRel of R2 = the InternalRel of R1
( the InternalRel of R2 c= the InternalRel of R1 & the InternalRel of R1 c= the InternalRel of R2 ) by Prop18, A1;
hence the InternalRel of R2 = the InternalRel of R1 by XBOOLE_0:def 10; :: thesis: verum