let T be TopStruct ; :: thesis: for M, N being Subset of holds M /\ N is Subset of
let M, N be Subset of ; :: thesis: M /\ N is Subset of
M /\ N c= N by XBOOLE_1:17;
then M /\ N c= [#] (T | N) by PRE_TOPC:def 10;
hence M /\ N is Subset of ; :: thesis: verum