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

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

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 `1 <= 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 `1 <= 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 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;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