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 A10: 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 A11: 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
A12: the carrier of R1 = the carrier of R2

proof

thus the carrier of R1 c= the carrier of R2 :: according to XBOOLE_0:def 10 :: thesis: 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 R1 or b in the carrier of R2 )
assume b in the carrier of R1 ; :: thesis: b in the carrier of R2
then consider s being Function of L,(InclPoset (Ids L)) such that
A13: ( b = s & s is monotone & ( for x being Element of L holds s . x c= downarrow x ) ) by A10;
thus b in the carrier of R2 by A11, A13; :: thesis: verum

end;

thus the carrier of R2 c= the carrier of R1 :: thesis: verum

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 consider s being Function of L,(InclPoset (Ids L)) such that
A14: ( b = s & s is monotone & ( for x being Element of L holds s . x c= downarrow x ) ) by A11;
thus b in the carrier of R1 by A10, A14; :: thesis: verum

end;

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 ) )

A15: now

assume [c,d] in the InternalRel of R1 ; :: thesis: [c,d] in the InternalRel of R2
then consider f, g being Function of L,(InclPoset (Ids L)) such that
A16: ( c = f & d = g & c in the carrier of R1 & d in the carrier of R1 & f <= g ) by A10;
thus [c,d] in the InternalRel of R2 by A11, A12, A16; :: thesis: verum

end;

now

assume [c,d] in the InternalRel of R2 ; :: thesis: [c,d] in the InternalRel of R1
then consider f, g being Function of L,(InclPoset (Ids L)) such that
A17: ( c = f & d = g & c in the carrier of R2 & d in the carrier of R2 & f <= g ) by A11;
thus [c,d] in the InternalRel of R1 by A10, A12, A17; :: 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 A15; :: thesis: verum

end;

hence R1 = R2 by A12; :: thesis: verum