let a, b, c, d be Real; :: 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 that
A1: a <= b and
A2: c <= d and
A3: p in rectangle (a,b,c,d) ; :: thesis: ( a <= p `1 & p `1 <= b & c <= p `2 & p `2 <= d )
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 A1, A2, A3, SPPOL_2:54;
then A4: ex p2 being Point of (TOP-REAL 2) st
( 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 ) ) ) ;

per cases ( ( p `1 = a & c <= p `2 & p `2 <= d ) or ( p `2 = d & a <= p `1 & p `1 <= b ) or ( p `1 = b & c <= p `2 & p `2 <= d ) or ( p `2 = c & a <= p `1 & p `1 <= b ) ) by A4;

suppose ( p `1 = a & c <= p `2 & p `2 <= d ) ; :: thesis: ( a <= p `1 & p `1 <= b & c <= p `2 & p `2 <= d )

hence ( a <= p `1 & p `1 <= b & c <= p `2 & p `2 <= d ) by A1; :: thesis: verum

end;

suppose ( p `2 = d & a <= p `1 & p `1 <= b ) ; :: thesis: ( a <= p `1 & p `1 <= b & c <= p `2 & p `2 <= d )

hence ( a <= p `1 & p `1 <= b & c <= p `2 & p `2 <= d ) by A2; :: thesis: verum

end;

suppose ( p `1 = b & c <= p `2 & p `2 <= d ) ; :: thesis: ( a <= p `1 & p `1 <= b & c <= p `2 & p `2 <= d )

hence ( a <= p `1 & p `1 <= b & c <= p `2 & p `2 <= d ) by A1; :: thesis: verum

end;

suppose ( p `2 = c & a <= p `1 & p `1 <= b ) ; :: thesis: ( a <= p `1 & p `1 <= b & c <= p `2 & p `2 <= d )

hence ( a <= p `1 & p `1 <= b & c <= p `2 & p `2 <= d ) by A2; :: thesis: verum

end;

end;