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

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