let a, b, c, d be real number ; :: thesis: ( 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 ; :: thesis: 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:77
.= (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 ; :: thesis: verum