let R1, R2 be strict RelStr ; :: thesis: ( ( for a being set holds
( ( a in the carrier of R1 implies ex s being Function of L,(InclPoset (Ids L)) st
( a = s & s is monotone & ( for x being Element of L holds s . x c= downarrow x ) ) ) & ( ex s being Function of L,(InclPoset (Ids L)) st
( a = s & s is monotone & ( for x being Element of L holds s . x c= downarrow x ) ) implies a in the carrier of R1 ) & ( for c, d being set holds
( [c,d] in the InternalRel of R1 iff ex f, g being Function of L,(InclPoset (Ids L)) st
( c = f & d = g & c in the carrier of R1 & d in the carrier of R1 & f <= g ) ) ) ) ) & ( for a being set holds
( ( a in the carrier of R2 implies ex s being Function of L,(InclPoset (Ids L)) st
( a = s & s is monotone & ( for x being Element of L holds s . x c= downarrow x ) ) ) & ( ex s being Function of L,(InclPoset (Ids L)) st
( a = s & s is monotone & ( for x being Element of L holds s . x c= downarrow x ) ) implies a in the carrier of R2 ) & ( for c, d being set holds
( [c,d] in the InternalRel of R2 iff ex f, g being Function of L,(InclPoset (Ids L)) st
( c = f & d = g & c in the carrier of R2 & d in the carrier of R2 & f <= g ) ) ) ) ) implies R1 = R2 )
assume A16: for a being set holds
( ( a in the carrier of R1 implies ex s being Function of L,(InclPoset (Ids L)) st
( a = s & s is monotone & ( for x being Element of L holds s . x c= downarrow x ) ) ) & ( ex s being Function of L,(InclPoset (Ids L)) st
( a = s & s is monotone & ( for x being Element of L holds s . x c= downarrow x ) ) implies a in the carrier of R1 ) & ( for c, d being set holds
( [c,d] in the InternalRel of R1 iff ex f, g being Function of L,(InclPoset (Ids L)) st
( c = f & d = g & c in the carrier of R1 & d in the carrier of R1 & f <= g ) ) ) ) ; :: thesis: ( ex a being set st
( ( a in the carrier of R2 implies ex s being Function of L,(InclPoset (Ids L)) st
( a = s & s is monotone & ( for x being Element of L holds s . x c= downarrow x ) ) ) & ( ex s being Function of L,(InclPoset (Ids L)) st
( a = s & s is monotone & ( for x being Element of L holds s . x c= downarrow x ) ) implies a in the carrier of R2 ) implies ex c, d being set st
( ( [c,d] in the InternalRel of R2 implies ex f, g being Function of L,(InclPoset (Ids L)) st
( c = f & d = g & c in the carrier of R2 & d in the carrier of R2 & f <= g ) ) implies ( ex f, g being Function of L,(InclPoset (Ids L)) st
( c = f & d = g & c in the carrier of R2 & d in the carrier of R2 & f <= g ) & not [c,d] in the InternalRel of R2 ) ) ) or R1 = R2 )
assume A17: for a being set holds
( ( a in the carrier of R2 implies ex s being Function of L,(InclPoset (Ids L)) st
( a = s & s is monotone & ( for x being Element of L holds s . x c= downarrow x ) ) ) & ( ex s being Function of L,(InclPoset (Ids L)) st
( a = s & s is monotone & ( for x being Element of L holds s . x c= downarrow x ) ) implies a in the carrier of R2 ) & ( for c, d being set holds
( [c,d] in the InternalRel of R2 iff ex f, g being Function of L,(InclPoset (Ids L)) st
( c = f & d = g & c in the carrier of R2 & d in the carrier of R2 & f <= g ) ) ) ) ; :: thesis: R1 = R2
A18: the carrier of R1 c= the carrier of R2

proof

let b be set ; :: according to TARSKI:def 3 :: thesis: ( not b in the carrier of R1 or b in the carrier of R2 )
assume b in the carrier of R1 ; :: thesis: b in the carrier of R2
then ex s being Function of L,(InclPoset (Ids L)) st
( b = s & s is monotone & ( for x being Element of L holds s . x c= downarrow x ) ) by A16;
hence b in the carrier of R2 by A17; :: thesis: verum

end;

A19: the carrier of R2 c= the carrier of R1

proof

let b be set ; :: according to TARSKI:def 3 :: thesis: ( not b in the carrier of R2 or b in the carrier of R1 )
assume b in the carrier of R2 ; :: thesis: b in the carrier of R1
then ex s being Function of L,(InclPoset (Ids L)) st
( b = s & s is monotone & ( for x being Element of L holds s . x c= downarrow x ) ) by A17;
hence b in the carrier of R1 by A16; :: thesis: verum

end;

the InternalRel of R1 = the InternalRel of R2

proof

let c, d be set ; :: according to RELAT_1:def 2 :: thesis: ( ( not [c,d] in the InternalRel of R1 or [c,d] in the InternalRel of R2 ) & ( not [c,d] in the InternalRel of R2 or [c,d] in the InternalRel of R1 ) )

A20: now

assume [c,d] in the InternalRel of R1 ; :: thesis: [c,d] in the InternalRel of R2
then ex f, g being Function of L,(InclPoset (Ids L)) st
( c = f & d = g & c in the carrier of R1 & d in the carrier of R1 & f <= g ) by A16;
hence [c,d] in the InternalRel of R2 by A17, A18; :: thesis: verum

end;

now

assume [c,d] in the InternalRel of R2 ; :: thesis: [c,d] in the InternalRel of R1
then ex f, g being Function of L,(InclPoset (Ids L)) st
( c = f & d = g & c in the carrier of R2 & d in the carrier of R2 & f <= g ) by A17;
hence [c,d] in the InternalRel of R1 by A16, A19; :: thesis: verum

end;

hence ( ( not [c,d] in the InternalRel of R1 or [c,d] in the InternalRel of R2 ) & ( not [c,d] in the InternalRel of R2 or [c,d] in the InternalRel of R1 ) ) by A20; :: thesis: verum

end;

hence R1 = R2 by A18, A19, XBOOLE_0:def 10; :: thesis: verum