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