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