let a, b, c, d be real number ; :: thesis: ( a <= b & c <= d implies rectangle a,b,c,d c= closed_inside_of_rectangle a,b,c,d )
assume A1: ( a <= b & c <= d ) ; :: thesis: rectangle a,b,c,d c= closed_inside_of_rectangle a,b,c,d
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in rectangle a,b,c,d or x in closed_inside_of_rectangle a,b,c,d )
assume x in rectangle a,b,c,d ; :: thesis: x in closed_inside_of_rectangle a,b,c,d
then x in { p where p is Point of (TOP-REAL 2) : ( ( p `1 = a & p `2 <= d & p `2 >= c ) or ( p `1 <= b & p `1 >= a & p `2 = d ) or ( p `1 <= b & p `1 >= a & p `2 = c ) or ( p `1 = b & p `2 <= d & p `2 >= c ) ) } by A1, SPPOL_2:58;
then ex p being Point of (TOP-REAL 2) st
( x = p & ( ( p `1 = a & p `2 <= d & p `2 >= c ) or ( p `1 <= b & p `1 >= a & p `2 = d ) or ( p `1 <= b & p `1 >= a & p `2 = c ) or ( p `1 = b & p `2 <= d & p `2 >= c ) ) ) ;
hence x in closed_inside_of_rectangle a,b,c,d by A1; :: thesis: verum