let a, b, c, d be Real; ( a <= b & c <= d implies rectangle (a,b,c,d) = { p where p is Point of (TOP-REAL 2) : ( ( 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 ) ) } )
set X = { p where p is Point of (TOP-REAL 2) : ( ( 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 ) ) } ;
assume that
A1:
a <= b
and
A2:
c <= d
; rectangle (a,b,c,d) = { p where p is Point of (TOP-REAL 2) : ( ( 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 ) ) }
A3:
rectangle (a,b,c,d) = { 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, SPPOL_2:54;
let x be object ; TARSKI:def 3 ( not x in { p where p is Point of (TOP-REAL 2) : ( ( 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 ) ) } or x in rectangle (a,b,c,d) )
assume
x in { p where p is Point of (TOP-REAL 2) : ( ( 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 ) ) }
; x in rectangle (a,b,c,d)
then
ex p being Point of (TOP-REAL 2) st
( x = p & ( ( 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 ) ) )
;
hence
x in rectangle (a,b,c,d)
by A3; verum