let T be 1-sorted ; :: thesis: for F, G being Subset-Family of T holds (union F) \ (union G) c= union (F \ G)
let F, G be Subset-Family of T; :: thesis: (union F) \ (union G) c= union (F \ G)
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (union F) \ (union G) or x in union (F \ G) )
assume A1: x in (union F) \ (union G) ; :: thesis: x in union (F \ G)
then x in union F by XBOOLE_0:def 5;
then consider A being set such that
A2: x in A and
A3: A in F by TARSKI:def 4;
not x in union G by A1, XBOOLE_0:def 5;
then not A in G by A2, TARSKI:def 4;
then A in F \ G by A3, XBOOLE_0:def 5;
hence x in union (F \ G) by A2, TARSKI:def 4; :: thesis: verum