let a, b, c, d be Real; :: thesis: closed_inside_of_rectangle (a,b,c,d) = (outside_of_rectangle (a,b,c,d)) `
set R = closed_inside_of_rectangle (a,b,c,d);
set O = outside_of_rectangle (a,b,c,d);
thus closed_inside_of_rectangle (a,b,c,d) c= (outside_of_rectangle (a,b,c,d)) ` :: according to XBOOLE_0:def 10 :: thesis: (outside_of_rectangle (a,b,c,d)) ` c= closed_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) or x in (outside_of_rectangle (a,b,c,d)) ` )
assume x in closed_inside_of_rectangle (a,b,c,d) ; :: thesis: x in (outside_of_rectangle (a,b,c,d)) `
then consider p being Point of (TOP-REAL 2) such that
A1: x = p and
A2: a <= p `1 and
A3: p `1 <= b and
A4: c <= p `2 and
A5: p `2 <= d ;
now :: thesis: not p in outside_of_rectangle (a,b,c,d)
assume p in outside_of_rectangle (a,b,c,d) ; :: thesis: contradiction
then ex p1 being Point of (TOP-REAL 2) st
( p1 = p & ( not a <= p1 `1 or not p1 `1 <= b or not c <= p1 `2 or not p1 `2 <= d ) ) ;
hence contradiction by A2, A3, A4, A5; :: thesis: verum
end;
hence x in (outside_of_rectangle (a,b,c,d)) ` by A1, SUBSET_1:29; :: thesis: verum
end;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (outside_of_rectangle (a,b,c,d)) ` or x in closed_inside_of_rectangle (a,b,c,d) )
assume A6: x in (outside_of_rectangle (a,b,c,d)) ` ; :: thesis: x in closed_inside_of_rectangle (a,b,c,d)
then A7: not x in outside_of_rectangle (a,b,c,d) by XBOOLE_0:def 5;
reconsider x = x as Point of (TOP-REAL 2) by A6;
A8: a <= x `1 by A7;
A9: x `1 <= b by A7;
A10: c <= x `2 by A7;
x `2 <= d by A7;
hence x in closed_inside_of_rectangle (a,b,c,d) by A8, A9, A10; :: thesis: verum