let a, b, c, d be Real; inside_of_rectangle (a,b,c,d) c= closed_inside_of_rectangle (a,b,c,d)
let x be object ; TARSKI:def 3 ( 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)
; 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)
; verum