let a, b, c, d be Real; :: thesis: inside_of_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 inside_of_rectangle (a,b,c,d) or x in closed_inside_of_rectangle (a,b,c,d) )
assume x in inside_of_rectangle (a,b,c,d) ; :: thesis: x in closed_inside_of_rectangle (a,b,c,d)
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 x in closed_inside_of_rectangle (a,b,c,d) ; :: thesis: verum