let GX be TopStruct ; :: thesis: for T, W being Subset of GX st T c= W holds
Int T c= Int W
let T, W be Subset of GX; :: thesis: ( T c= W implies Int T c= Int W )
assume T c= W ; :: thesis: Int T c= Int W
then W ` c= T ` by SUBSET_1:12;
then Cl (W `) c= Cl (T `) by PRE_TOPC:19;
hence Int T c= Int W by SUBSET_1:12; :: thesis: verum