let GX be TopStruct ; :: thesis: for S, T being Subset of st S is open & S c= T holds
S c= Int T
let S, T be Subset of ; :: 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, Th55;
hence S c= Int T by A2, Th48; :: thesis: verum