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 ) ) ) ;

( 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;

end;

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

end;

end;

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

end;

end;