let s1 be Real; :: thesis: for P1, P2 being Subset of (TOP-REAL 2) st P1 = { |[s,r]| where s, r is Real : s <= s1 } & P2 = { |[s2,r2]| where s2, r2 is Real : s2 > s1 } holds
P1 = P2 `
let P1, P2 be Subset of (TOP-REAL 2); :: thesis: ( P1 = { |[s,r]| where s, r is Real : s <= s1 } & P2 = { |[s2,r2]| where s2, r2 is Real : s2 > s1 } implies P1 = P2 ` )
assume A1: ( P1 = { |[s,r]| where s, r is Real : s <= s1 } & P2 = { |[s2,r2]| where s2, r2 is Real : s2 > s1 } ) ; :: thesis: P1 = P2 `
A2: P2 ` c= P1
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in P2 ` or x in P1 )
assume A3: x in P2 ` ; :: thesis: x in P1
then reconsider p = x as Point of (TOP-REAL 2) ;
A4: p = |[(p `1),(p `2)]| by EUCLID:53;
x in the carrier of (TOP-REAL 2) \ P2 by A3, SUBSET_1:def 4;
then not x in P2 by XBOOLE_0:def 5;
then p `1 <= s1 by A1, A4;
hence x in P1 by A1, A4; :: thesis: verum
end;
P1 c= P2 `
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in P1 or x in P2 ` )
assume A5: x in P1 ; :: thesis: x in P2 `
then ex s, r being Real st
( |[s,r]| = x & s <= s1 ) by A1;
then for s2, r2 being Real holds
( not |[s2,r2]| = x or not s2 > s1 ) by SPPOL_2:1;
then not x in { |[s2,r2]| where s2, r2 is Real : s2 > s1 } ;
then x in the carrier of (TOP-REAL 2) \ P2 by A1, A5, XBOOLE_0:def 5;
hence x in P2 ` by SUBSET_1:def 4; :: thesis: verum
end;
hence P1 = P2 ` by A2; :: thesis: verum