let T be TopStruct ; :: thesis: for A being Subset of T holds Fr A = (Cl A) \ (Int A)
let A be Subset of T; :: thesis: Fr A = (Cl A) \ (Int A)
Fr A = (Cl A) /\ (((Cl (A `)) `) `) by TOPS_1:def 2
.= (Cl A) \ ((Cl (A `)) `) by SUBSET_1:13
.= (Cl A) \ (Int A) by TOPS_1:def 1 ;
hence Fr A = (Cl A) \ (Int A) ; :: thesis: verum