let a, b, c, d be Real; :: thesis: ( a <= b & c <= d implies rectangle (a,b,c,d) c= closed_inside_of_rectangle (a,b,c,d) )
assume that
A1: a <= b and
A2: c <= d ; :: thesis: rectangle (a,b,c,d) c= closed_inside_of_rectangle (a,b,c,d)
let x be object ; :: 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, A2, SPPOL_2:54;
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, A2; :: thesis: verum