let T be TopStruct ; :: thesis: for Q, M being Subset of T
for F being Subset-Family of T st Q in F holds
Q /\ M in F | M
let Q, M be Subset of T; :: thesis: for F being Subset-Family of T st Q in F holds
Q /\ M in F | M
let F be Subset-Family of T; :: thesis: ( Q in F implies Q /\ M in F | M )
reconsider QQ = Q /\ M as Subset of (T | M) by Th29;
A1: Q /\ M = QQ ;
assume Q in F ; :: thesis: Q /\ M in F | M
hence Q /\ M in F | M by A1, Def3; :: thesis: verum