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