let a, b, c, d be Real; ( a < b & c < d implies Fr (closed_inside_of_rectangle (a,b,c,d)) = rectangle (a,b,c,d) )
assume that
A1:
a < b
and
A2:
c < d
; Fr (closed_inside_of_rectangle (a,b,c,d)) = rectangle (a,b,c,d)
set P = closed_inside_of_rectangle (a,b,c,d);
thus Fr (closed_inside_of_rectangle (a,b,c,d)) =
(closed_inside_of_rectangle (a,b,c,d)) \ (Int (closed_inside_of_rectangle (a,b,c,d)))
by TOPS_1:43
.=
(closed_inside_of_rectangle (a,b,c,d)) \ (inside_of_rectangle (a,b,c,d))
by A1, A2, Th50
.=
rectangle (a,b,c,d)
by A1, A2, Th51
; verum