let a, b, c, d be Real; :: thesis: ( a <= b & c <= d implies (closed_inside_of_rectangle (a,b,c,d)) \ (inside_of_rectangle (a,b,c,d)) = rectangle (a,b,c,d) )
assume that
A1: a <= b and
A2: c <= d ; :: thesis: (closed_inside_of_rectangle (a,b,c,d)) \ (inside_of_rectangle (a,b,c,d)) = rectangle (a,b,c,d)
set R = rectangle (a,b,c,d);
set P = closed_inside_of_rectangle (a,b,c,d);
set P1 = inside_of_rectangle (a,b,c,d);
A3: rectangle (a,b,c,d) = { 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;
thus (closed_inside_of_rectangle (a,b,c,d)) \ (inside_of_rectangle (a,b,c,d)) c= rectangle (a,b,c,d) :: according to XBOOLE_0:def 10 :: thesis: rectangle (a,b,c,d) c= (closed_inside_of_rectangle (a,b,c,d)) \ (inside_of_rectangle (a,b,c,d))
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (closed_inside_of_rectangle (a,b,c,d)) \ (inside_of_rectangle (a,b,c,d)) or x in rectangle (a,b,c,d) )
assume A4: x in (closed_inside_of_rectangle (a,b,c,d)) \ (inside_of_rectangle (a,b,c,d)) ; :: thesis: x in rectangle (a,b,c,d)
then A5: not x in inside_of_rectangle (a,b,c,d) by XBOOLE_0:def 5;
x in closed_inside_of_rectangle (a,b,c,d) by A4, XBOOLE_0:def 5;
then consider p being Point of (TOP-REAL 2) such that
A6: x = p and
A7: a <= p `1 and
A8: p `1 <= b and
A9: c <= p `2 and
A10: p `2 <= d ;
( not a < p `1 or not p `1 < b or not c < p `2 or not p `2 < d ) by A5, A6;
then ( ( 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 A7, A8, A9, A10, XXREAL_0:1;
hence x in rectangle (a,b,c,d) by A3, A6; :: thesis: verum
end;
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)) \ (inside_of_rectangle (a,b,c,d)) )
assume A11: x in rectangle (a,b,c,d) ; :: thesis: x in (closed_inside_of_rectangle (a,b,c,d)) \ (inside_of_rectangle (a,b,c,d))
then A12: ex p being Point of (TOP-REAL 2) st
( p = x & ( ( 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 A3;
A13: rectangle (a,b,c,d) c= closed_inside_of_rectangle (a,b,c,d) by A1, A2, Th45;
now :: thesis: not x in inside_of_rectangle (a,b,c,d)
assume x in inside_of_rectangle (a,b,c,d) ; :: thesis: contradiction
then ex p being Point of (TOP-REAL 2) st
( x = p & a < p `1 & p `1 < b & c < p `2 & p `2 < d ) ;
hence contradiction by A12; :: thesis: verum
end;
hence x in (closed_inside_of_rectangle (a,b,c,d)) \ (inside_of_rectangle (a,b,c,d)) by A11, A13, XBOOLE_0:def 5; :: thesis: verum