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 A1: ( a < b & 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, Th50
.= rectangle a,b,c,d by A1, Th51 ; :: thesis: verum