let GX be TopStruct ; :: thesis: for S, T being Subset of GX st S is open & S c= T holds
S c= Int T
let S, T be Subset of GX; :: thesis: ( S is open & S c= T implies S c= Int T )
assume A1: ( S is open & S c= T ) ; :: thesis: S c= Int T
then Int S = S by Th55;
hence S c= Int T by A1, Th48; :: thesis: verum