let s1, s2, t1, t2 be Real; :: thesis: { p where p is Point of (TOP-REAL 2) : ( s1 < p `1 & p `1 < s2 & t1 < p `2 & p `2 < t2 ) } = { |[sa,ta]| where sa, ta is Real : ( s1 < sa & sa < s2 & t1 < ta & ta < t2 ) }
now :: thesis: for x being object holds
( x in { p where p is Point of (TOP-REAL 2) : ( s1 < p `1 & p `1 < s2 & t1 < p `2 & p `2 < t2 ) } iff x in { |[sa,ta]| where sa, ta is Real : ( s1 < sa & sa < s2 & t1 < ta & ta < t2 ) } )
let x be object ; :: thesis: ( x in { p where p is Point of (TOP-REAL 2) : ( s1 < p `1 & p `1 < s2 & t1 < p `2 & p `2 < t2 ) } iff x in { |[sa,ta]| where sa, ta is Real : ( s1 < sa & sa < s2 & t1 < ta & ta < t2 ) } )
A1: now :: thesis: ( x in { p where p is Point of (TOP-REAL 2) : ( s1 < p `1 & p `1 < s2 & t1 < p `2 & p `2 < t2 ) } implies x in { |[s1a,t1a]| where s1a, t1a is Real : ( s1 < s1a & s1a < s2 & t1 < t1a & t1a < t2 ) } )
assume x in { p where p is Point of (TOP-REAL 2) : ( s1 < p `1 & p `1 < s2 & t1 < p `2 & p `2 < t2 ) } ; :: thesis: x in { |[s1a,t1a]| where s1a, t1a is Real : ( s1 < s1a & s1a < s2 & t1 < t1a & t1a < t2 ) }
then consider pp being Point of (TOP-REAL 2) such that
A2: pp = x and
A3: s1 < pp `1 and
A4: pp `1 < s2 and
A5: t1 < pp `2 and
A6: pp `2 < t2 ;
|[(pp `1),(pp `2)]| = x by A2, EUCLID:53;
hence x in { |[s1a,t1a]| where s1a, t1a is Real : ( s1 < s1a & s1a < s2 & t1 < t1a & t1a < t2 ) } by A3, A4, A5, A6; :: thesis: verum
end;
now :: thesis: ( x in { |[sa,ta]| where sa, ta is Real : ( s1 < sa & sa < s2 & t1 < ta & ta < t2 ) } implies x in { p where p is Point of (TOP-REAL 2) : ( s1 < p `1 & p `1 < s2 & t1 < p `2 & p `2 < t2 ) } )
assume x in { |[sa,ta]| where sa, ta is Real : ( s1 < sa & sa < s2 & t1 < ta & ta < t2 ) } ; :: thesis: x in { p where p is Point of (TOP-REAL 2) : ( s1 < p `1 & p `1 < s2 & t1 < p `2 & p `2 < t2 ) }
then consider sa, ta being Real such that
A7: |[sa,ta]| = x and
A8: s1 < sa and
A9: sa < s2 and
A10: t1 < ta and
A11: ta < t2 ;
set pa = |[sa,ta]|;
A12: s1 < |[sa,ta]| `1 by A8, EUCLID:52;
A13: |[sa,ta]| `1 < s2 by A9, EUCLID:52;
A14: t1 < |[sa,ta]| `2 by A10, EUCLID:52;
|[sa,ta]| `2 < t2 by A11, EUCLID:52;
hence x in { p where p is Point of (TOP-REAL 2) : ( s1 < p `1 & p `1 < s2 & t1 < p `2 & p `2 < t2 ) } by A7, A12, A13, A14; :: thesis: verum
end;
hence ( x in { p where p is Point of (TOP-REAL 2) : ( s1 < p `1 & p `1 < s2 & t1 < p `2 & p `2 < t2 ) } iff x in { |[sa,ta]| where sa, ta is Real : ( s1 < sa & sa < s2 & t1 < ta & ta < t2 ) } ) by A1; :: thesis: verum
end;
hence { p where p is Point of (TOP-REAL 2) : ( s1 < p `1 & p `1 < s2 & t1 < p `2 & p `2 < t2 ) } = { |[sa,ta]| where sa, ta is Real : ( s1 < sa & sa < s2 & t1 < ta & ta < t2 ) } by TARSKI:2; :: thesis: verum