let a, b, c, d be real number ; :: thesis: for p being Point of (TOP-REAL 2) st a <= b & c <= d & p in rectangle a,b,c,d holds
( a <= p `1 & p `1 <= b & c <= p `2 & p `2 <= d )
let p be Point of (TOP-REAL 2); :: thesis: ( a <= b & c <= d & p in rectangle a,b,c,d implies ( a <= p `1 & p `1 <= b & c <= p `2 & p `2 <= d ) )
assume A1:
( a <= b & c <= d & p in rectangle a,b,c,d )
; :: thesis: ( a <= p `1 & p `1 <= b & c <= p `2 & p `2 <= d )
then
p in { p2 where p2 is Point of (TOP-REAL 2) : ( ( p2 `1 = a & p2 `2 <= d & p2 `2 >= c ) or ( p2 `1 <= b & p2 `1 >= a & p2 `2 = d ) or ( p2 `1 <= b & p2 `1 >= a & p2 `2 = c ) or ( p2 `1 = b & p2 `2 <= d & p2 `2 >= c ) ) }
by SPPOL_2:58;
then consider p2 being Point of (TOP-REAL 2) such that
A2:
( p2 = p & ( ( p2 `1 = a & p2 `2 <= d & p2 `2 >= c ) or ( p2 `1 <= b & p2 `1 >= a & p2 `2 = d ) or ( p2 `1 <= b & p2 `1 >= a & p2 `2 = c ) or ( p2 `1 = b & p2 `2 <= d & p2 `2 >= c ) ) )
;