let T be TopStruct ; :: thesis: for Q, M being Subset of T
for F being Subset-Family of T st Q c= union F holds
Q /\ M c= union (F | M)
let Q, M be Subset of T; :: thesis: for F being Subset-Family of T st Q c= union F holds
Q /\ M c= union (F | M)
let F be Subset-Family of T; :: thesis: ( Q c= union F implies Q /\ M c= union (F | M) )
assume A1: Q c= union F ; :: thesis: Q /\ M c= union (F | M)
now :: thesis: ( M <> {} implies Q /\ M c= union (F | M) )
assume M <> {} ; :: thesis: Q /\ M c= union (F | M)
thus Q /\ M c= union (F | M) :: thesis: verum
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Q /\ M or x in union (F | M) )
assume A2: x in Q /\ M ; :: thesis: x in union (F | M)
then x in Q by XBOOLE_0:def 4;
then consider Z being set such that
A3: x in Z and
A4: Z in F by A1, TARSKI:def 4;
reconsider ZZ = Z as Subset of T by A4;
ZZ /\ M in F | M by A4, Th31;
then reconsider ZP = ZZ /\ M as Subset of (T | M) ;
A5: ZP in F | M by A4, Th31;
x in M by A2, XBOOLE_0:def 4;
then x in ZP by A3, XBOOLE_0:def 4;
hence x in union (F | M) by A5, TARSKI:def 4; :: thesis: verum
end;
end;
hence Q /\ M c= union (F | M) ; :: thesis: verum