let s1, s2, t1, t2 be Real; { 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 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 ;
( 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 ( 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 ) } )end; now ( 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 ) }
;
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;
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;
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; verum