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 that
A1: S is open and
A2: S c= T ; :: thesis: S c= Int T
Int S = S by A1, Th23;
hence S c= Int T by A2, Th19; :: thesis: verum