let a, b, c, d be Real; 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); ( 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)
; ( 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 ) ) )
;