let a, b, c, d be real number ; :: thesis: ( 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 ; :: thesis: 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:58;

hereby :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis: { 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 ) ) } c= rectangle a,b,c,d

let x be set ; :: thesis: ( x in rectangle a,b,c,d implies 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 ) ) } )
assume x in rectangle a,b,c,d ; :: thesis: 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 ) ) }
then ex p2 being Point of (TOP-REAL 2) st
( x = p2 & ( ( 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 A3;
hence 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 ) ) } ; :: thesis: verum

end;

let x be set ; :: according to TARSKI:def 3 :: thesis: ( 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 ) ) } ; :: thesis: 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; :: thesis: verum