let s1 be Real; :: thesis: for P1, P2 being Subset of (TOP-REAL 2) st P1 = { |[r,s]| where r, s is Real : s >= s1 } & P2 = { |[r2,s2]| where r2, s2 is Real : s2 < s1 } holds
P1 = P2 `
let P1, P2 be Subset of (TOP-REAL 2); :: thesis: ( P1 = { |[r,s]| where r, s is Real : s >= s1 } & P2 = { |[r2,s2]| where r2, s2 is Real : s2 < s1 } implies P1 = P2 ` )
assume A1: ( P1 = { |[r,s]| where r, s is Real : s >= s1 } & P2 = { |[r2,s2]| where r2, s2 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 `2 >= 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 r, s being Real st
( |[r,s]| = x & s >= s1 ) by A1;
then for r2, s2 being Real holds
( not |[r2,s2]| = x or not s2 < s1 ) by SPPOL_2:1;
then not x in P2 by A1;
then x in the carrier of (TOP-REAL 2) \ P2 by A5, XBOOLE_0:def 5;
hence x in P2 ` by SUBSET_1:def 4; :: thesis: verum
end;
hence P1 = P2 ` by A2; :: thesis: verum