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