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 set ; :: according to TARSKI:def 3 :: thesis: ( not x in (union F) \ (union G) or x in union (F \ G) )
assume x in (union F) \ (union G) ; :: thesis: x in union (F \ G)
then A1: ( x in union F & not x in union G ) by XBOOLE_0:def 5;
then consider A being set such that
A2: ( x in A & A in F ) by TARSKI:def 4;
not A in G by A1, A2, TARSKI:def 4;
then ( x in A & A in F \ G ) by A2, XBOOLE_0:def 5;
hence x in union (F \ G) by TARSKI:def 4; :: thesis: verum