let s1 be Real; :: thesis: for P1, P2 being Subset of () 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 (); :: 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 () ;
A4: p = |[(p `1),(p `2)]| by EUCLID:53;
x in the carrier of () \ P2 by ;
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 () \ P2 by ;
hence x in P2 ` by SUBSET_1:def 4; :: thesis: verum
end;
hence P1 = P2 ` by A2; :: thesis: verum