let T be TopStruct ; :: thesis: for M being Subset of T
for F being Subset-Family of T holds union (F | M) c= union F
let M be Subset of T; :: thesis: for F being Subset-Family of T holds union (F | M) c= union F
let F be Subset-Family of T; :: thesis: union (F | M) c= union F
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in union (F | M) or x in union F )
assume x in union (F | M) ; :: thesis: x in union F
then consider A being set such that
A1: x in A and
A2: A in F | M by TARSKI:def 4;
reconsider Q = A as Subset of (T | M) by A2;
consider R being Subset of T such that
A3: R in F and
A4: R /\ M = Q by A2, Def3;
x in R by A1, A4, XBOOLE_0:def 4;
hence x in union F by A3, TARSKI:def 4; :: thesis: verum