let s1, s2, t1, t2 be Real; :: thesis: { |[s,t]| where s, t is Real : ( s1 < s & s < s2 & t1 < t & t < t2 ) } is Subset of (REAL 2)
{ |[sb,tb]| where sb, tb is Real : ( s1 < sb & sb < s2 & t1 < tb & tb < t2 ) } c= REAL 2
proof
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in { |[sb,tb]| where sb, tb is Real : ( s1 < sb & sb < s2 & t1 < tb & tb < t2 ) } or y in REAL 2 )
assume y in { |[sb,tb]| where sb, tb is Real : ( s1 < sb & sb < s2 & t1 < tb & tb < t2 ) } ; :: thesis: y in REAL 2
then consider s7, t7 being Real such that
A1: |[s7,t7]| = y and
s1 < s7 and
s7 < s2 and
t1 < t7 and
t7 < t2 ;
|[s7,t7]| in the carrier of (TOP-REAL 2) ;
hence y in REAL 2 by A1, EUCLID:22; :: thesis: verum
end;
hence { |[s,t]| where s, t is Real : ( s1 < s & s < s2 & t1 < t & t < t2 ) } is Subset of (REAL 2) ; :: thesis: verum