let s1 be Real; 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); ( 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 } )
; P1 = P2 `
A2:
P2 ` c= P1
P1 c= P2 `
hence
P1 = P2 `
by A2; verum