let a, b, c, d be Real; :: thesis: for p being Point of () 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 (); :: 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 () : ( ( 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 ;
then A4: ex p2 being Point of () 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;