let s1, s2, t1, t2 be Real; :: thesis: { qc where qc is Point of (TOP-REAL 2) : ( not s1 <= qc `1 or not qc `1 <= s2 or not t1 <= qc `2 or not qc `2 <= t2 ) } = { |[sb,tb]| where sb, tb is Real : ( not s1 <= sb or not sb <= s2 or not t1 <= tb or not tb <= t2 ) }

now :: thesis: for x being object holds
( x in { qc where qc is Point of (TOP-REAL 2) : ( not s1 <= qc `1 or not qc `1 <= s2 or not t1 <= qc `2 or not qc `2 <= t2 ) } iff x in { |[sb,tb]| where sb, tb is Real : ( not s1 <= sb or not sb <= s2 or not t1 <= tb or not tb <= t2 ) } )

let x be object ; :: thesis: ( x in { qc where qc is Point of (TOP-REAL 2) : ( not s1 <= qc `1 or not qc `1 <= s2 or not t1 <= qc `2 or not qc `2 <= t2 ) } iff x in { |[sb,tb]| where sb, tb is Real : ( not s1 <= sb or not sb <= s2 or not t1 <= tb or not tb <= t2 ) } )

A1: now :: thesis: ( x in { qc where qc is Point of (TOP-REAL 2) : ( not s1 <= qc `1 or not qc `1 <= s2 or not t1 <= qc `2 or not qc `2 <= t2 ) } implies x in { |[s2a,t2a]| where s2a, t2a is Real : ( not s1 <= s2a or not s2a <= s2 or not t1 <= t2a or not t2a <= t2 ) } )

assume x in { qc where qc is Point of (TOP-REAL 2) : ( not s1 <= qc `1 or not qc `1 <= s2 or not t1 <= qc `2 or not qc `2 <= t2 ) } ; :: thesis: x in { |[s2a,t2a]| where s2a, t2a is Real : ( not s1 <= s2a or not s2a <= s2 or not t1 <= t2a or not t2a <= t2 ) }
then consider q being Point of (TOP-REAL 2) such that
A2: q = x and
A3: ( not s1 <= q `1 or not q `1 <= s2 or not t1 <= q `2 or not q `2 <= t2 ) ;
|[(q `1),(q `2)]| = x by A2, EUCLID:53;
hence x in { |[s2a,t2a]| where s2a, t2a is Real : ( not s1 <= s2a or not s2a <= s2 or not t1 <= t2a or not t2a <= t2 ) } by A3; :: thesis: verum

end;

now :: thesis: ( x in { |[sb,tb]| where sb, tb is Real : ( not s1 <= sb or not sb <= s2 or not t1 <= tb or not tb <= t2 ) } implies x in { qc where qc is Point of (TOP-REAL 2) : ( not s1 <= qc `1 or not qc `1 <= s2 or not t1 <= qc `2 or not qc `2 <= t2 ) } )

assume x in { |[sb,tb]| where sb, tb is Real : ( not s1 <= sb or not sb <= s2 or not t1 <= tb or not tb <= t2 ) } ; :: thesis: x in { qc where qc is Point of (TOP-REAL 2) : ( not s1 <= qc `1 or not qc `1 <= s2 or not t1 <= qc `2 or not qc `2 <= t2 ) }
then consider sb, tb being Real such that
A4: |[sb,tb]| = x and
A5: ( not s1 <= sb or not sb <= s2 or not t1 <= tb or not tb <= t2 ) ;
set qa = |[sb,tb]|;
( not s1 <= |[sb,tb]| `1 or not |[sb,tb]| `1 <= s2 or not t1 <= |[sb,tb]| `2 or not |[sb,tb]| `2 <= t2 ) by A5, EUCLID:52;
hence x in { qc where qc is Point of (TOP-REAL 2) : ( not s1 <= qc `1 or not qc `1 <= s2 or not t1 <= qc `2 or not qc `2 <= t2 ) } by A4; :: thesis: verum

end;

hence ( x in { qc where qc is Point of (TOP-REAL 2) : ( not s1 <= qc `1 or not qc `1 <= s2 or not t1 <= qc `2 or not qc `2 <= t2 ) } iff x in { |[sb,tb]| where sb, tb is Real : ( not s1 <= sb or not sb <= s2 or not t1 <= tb or not tb <= t2 ) } ) by A1; :: thesis: verum

end;

hence { qc where qc is Point of (TOP-REAL 2) : ( not s1 <= qc `1 or not qc `1 <= s2 or not t1 <= qc `2 or not qc `2 <= t2 ) } = { |[sb,tb]| where sb, tb is Real : ( not s1 <= sb or not sb <= s2 or not t1 <= tb or not tb <= t2 ) } by TARSKI:2; :: thesis: verum