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 object 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 object 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 A13: 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 object 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 object 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 A14: 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 object 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
A15: the carrier of R1 c= the carrier of R2
proof
let b be object ; :: 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 A13;
hence b in the carrier of R2 by A14; :: thesis: verum
end;
A16: the carrier of R2 c= the carrier of R1
proof
let b be object ; :: 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 A14;
hence b in the carrier of R1 by A13; :: thesis: verum
end;
the InternalRel of R1 = the InternalRel of R2
proof
let c, d be object ; :: 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 ) )
A17: now :: thesis: ( [c,d] in the InternalRel of R1 implies [c,d] in the InternalRel of R2 )
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 A13;
hence [c,d] in the InternalRel of R2 by A14, A15; :: thesis: verum
end;
now :: thesis: ( [c,d] in the InternalRel of R2 implies [c,d] in the InternalRel of R1 )
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 A14;
hence [c,d] in the InternalRel of R1 by A13, A16; :: 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 A17; :: thesis: verum
end;
hence R1 = R2 by A15, A16, XBOOLE_0:def 10; :: thesis: verum