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

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

P1 c= P2 `
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;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

proof

hence
P1 = P2 `
by A2; :: thesis: verum
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;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