let s1, t1, s2, t2 be Real; { |[s,t]| where s, t is Real : ( s1 < s & s < s2 & t1 < t & t < t2 ) } = (( { |[s3,t3]| where s3, t3 is Real : s1 < s3 } /\ { |[s4,t4]| where s4, t4 is Real : s4 < s2 } ) /\ { |[s5,t5]| where s5, t5 is Real : t1 < t5 } ) /\ { |[s6,t6]| where s6, t6 is Real : t6 < t2 }
now for x being object st x in { |[s,t]| where s, t is Real : ( s1 < s & s < s2 & t1 < t & t < t2 ) } holds
x in (( { |[s3,t3]| where s3, t3 is Real : s1 < s3 } /\ { |[s4,t4]| where s4, t4 is Real : s4 < s2 } ) /\ { |[s5,t5]| where s5, t5 is Real : t1 < t5 } ) /\ { |[s6,t6]| where s6, t6 is Real : t6 < t2 } let x be
object ;
( x in { |[s,t]| where s, t is Real : ( s1 < s & s < s2 & t1 < t & t < t2 ) } implies x in (( { |[s3,t3]| where s3, t3 is Real : s1 < s3 } /\ { |[s4,t4]| where s4, t4 is Real : s4 < s2 } ) /\ { |[s5,t5]| where s5, t5 is Real : t1 < t5 } ) /\ { |[s6,t6]| where s6, t6 is Real : t6 < t2 } )assume
x in { |[s,t]| where s, t is Real : ( s1 < s & s < s2 & t1 < t & t < t2 ) }
;
x in (( { |[s3,t3]| where s3, t3 is Real : s1 < s3 } /\ { |[s4,t4]| where s4, t4 is Real : s4 < s2 } ) /\ { |[s5,t5]| where s5, t5 is Real : t1 < t5 } ) /\ { |[s6,t6]| where s6, t6 is Real : t6 < t2 } then A1:
ex
s,
t being
Real st
(
|[s,t]| = x &
s1 < s &
s < s2 &
t1 < t &
t < t2 )
;
then A2:
x in { |[s3,t3]| where s3, t3 is Real : s1 < s3 }
;
x in { |[s4,t4]| where s4, t4 is Real : s4 < s2 }
by A1;
then A3:
x in { |[s3,t3]| where s3, t3 is Real : s1 < s3 } /\ { |[s4,t4]| where s4, t4 is Real : s4 < s2 }
by A2, XBOOLE_0:def 4;
A4:
x in { |[s5,t5]| where s5, t5 is Real : t1 < t5 }
by A1;
A5:
x in { |[s6,t6]| where s6, t6 is Real : t6 < t2 }
by A1;
x in ( { |[s3,t3]| where s3, t3 is Real : s1 < s3 } /\ { |[s4,t4]| where s4, t4 is Real : s4 < s2 } ) /\ { |[s5,t5]| where s5, t5 is Real : t1 < t5 }
by A3, A4, XBOOLE_0:def 4;
hence
x in (( { |[s3,t3]| where s3, t3 is Real : s1 < s3 } /\ { |[s4,t4]| where s4, t4 is Real : s4 < s2 } ) /\ { |[s5,t5]| where s5, t5 is Real : t1 < t5 } ) /\ { |[s6,t6]| where s6, t6 is Real : t6 < t2 }
by A5, XBOOLE_0:def 4;
verum end;
then A6:
{ |[s,t]| where s, t is Real : ( s1 < s & s < s2 & t1 < t & t < t2 ) } c= (( { |[s3,t3]| where s3, t3 is Real : s1 < s3 } /\ { |[s4,t4]| where s4, t4 is Real : s4 < s2 } ) /\ { |[s5,t5]| where s5, t5 is Real : t1 < t5 } ) /\ { |[s6,t6]| where s6, t6 is Real : t6 < t2 }
;
now for x being object st x in (( { |[s3,t3]| where s3, t3 is Real : s1 < s3 } /\ { |[s4,t4]| where s4, t4 is Real : s4 < s2 } ) /\ { |[s5,t5]| where s5, t5 is Real : t1 < t5 } ) /\ { |[s6,t6]| where s6, t6 is Real : t6 < t2 } holds
x in { |[s,t]| where s, t is Real : ( s1 < s & s < s2 & t1 < t & t < t2 ) } let x be
object ;
( x in (( { |[s3,t3]| where s3, t3 is Real : s1 < s3 } /\ { |[s4,t4]| where s4, t4 is Real : s4 < s2 } ) /\ { |[s5,t5]| where s5, t5 is Real : t1 < t5 } ) /\ { |[s6,t6]| where s6, t6 is Real : t6 < t2 } implies x in { |[s,t]| where s, t is Real : ( s1 < s & s < s2 & t1 < t & t < t2 ) } )assume A7:
x in (( { |[s3,t3]| where s3, t3 is Real : s1 < s3 } /\ { |[s4,t4]| where s4, t4 is Real : s4 < s2 } ) /\ { |[s5,t5]| where s5, t5 is Real : t1 < t5 } ) /\ { |[s6,t6]| where s6, t6 is Real : t6 < t2 }
;
x in { |[s,t]| where s, t is Real : ( s1 < s & s < s2 & t1 < t & t < t2 ) } then A8:
x in ( { |[s3,t3]| where s3, t3 is Real : s1 < s3 } /\ { |[s4,t4]| where s4, t4 is Real : s4 < s2 } ) /\ { |[s5,t5]| where s5, t5 is Real : t1 < t5 }
by XBOOLE_0:def 4;
then A9:
x in { |[s3,t3]| where s3, t3 is Real : s1 < s3 } /\ { |[s4,t4]| where s4, t4 is Real : s4 < s2 }
by XBOOLE_0:def 4;
A10:
x in { |[s6,t6]| where s6, t6 is Real : t6 < t2 }
by A7, XBOOLE_0:def 4;
A11:
x in { |[s3,t3]| where s3, t3 is Real : s1 < s3 }
by A9, XBOOLE_0:def 4;
A12:
x in { |[s4,t4]| where s4, t4 is Real : s4 < s2 }
by A9, XBOOLE_0:def 4;
A13:
x in { |[s5,t5]| where s5, t5 is Real : t1 < t5 }
by A8, XBOOLE_0:def 4;
A14:
ex
sa,
ta being
Real st
(
|[sa,ta]| = x &
s1 < sa )
by A11;
A15:
ex
sb,
tb being
Real st
(
|[sb,tb]| = x &
sb < s2 )
by A12;
A16:
ex
sc,
tc being
Real st
(
|[sc,tc]| = x &
t1 < tc )
by A13;
A17:
ex
sd,
td being
Real st
(
|[sd,td]| = x &
td < t2 )
by A10;
consider sa,
ta being
Real such that A18:
|[sa,ta]| = x
and A19:
s1 < sa
by A11;
reconsider p =
x as
Point of
(TOP-REAL 2) by A14;
A20:
p `1 = sa
by A18, EUCLID:52;
A21:
p `2 = ta
by A18, EUCLID:52;
A22:
sa < s2
by A15, A20, EUCLID:52;
A23:
t1 < ta
by A16, A21, EUCLID:52;
ta < t2
by A17, A21, EUCLID:52;
hence
x in { |[s,t]| where s, t is Real : ( s1 < s & s < s2 & t1 < t & t < t2 ) }
by A18, A19, A22, A23;
verum end;
then
(( { |[s3,t3]| where s3, t3 is Real : s1 < s3 } /\ { |[s4,t4]| where s4, t4 is Real : s4 < s2 } ) /\ { |[s5,t5]| where s5, t5 is Real : t1 < t5 } ) /\ { |[s6,t6]| where s6, t6 is Real : t6 < t2 } c= { |[s,t]| where s, t is Real : ( s1 < s & s < s2 & t1 < t & t < t2 ) }
;
hence
{ |[s,t]| where s, t is Real : ( s1 < s & s < s2 & t1 < t & t < t2 ) } = (( { |[s3,t3]| where s3, t3 is Real : s1 < s3 } /\ { |[s4,t4]| where s4, t4 is Real : s4 < s2 } ) /\ { |[s5,t5]| where s5, t5 is Real : t1 < t5 } ) /\ { |[s6,t6]| where s6, t6 is Real : t6 < t2 }
by A6; verum