let F, G be set ; :: thesis: ( F <> {} & G <> {} implies () \/ () = union (UNION (F,G)) )
assume that
A1: F <> {} and
A2: G <> {} ; :: thesis: () \/ () = union (UNION (F,G))
thus (union F) \/ () c= union (UNION (F,G)) :: according to XBOOLE_0:def 10 :: thesis: union (UNION (F,G)) c= () \/ ()
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in () \/ () or x in union (UNION (F,G)) )
assume A3: x in () \/ () ; :: thesis: x in union (UNION (F,G))
per cases ( x in union F or x in union G ) by ;
suppose A4: x in union F ; :: thesis: x in union (UNION (F,G))
consider W being object such that
A5: W in G by ;
consider Y being set such that
A6: x in Y and
A7: Y in F by ;
reconsider Y = Y, W = W as set by TARSKI:1;
set YW = Y \/ W;
( Y c= Y \/ W & Y \/ W in UNION (F,G) ) by ;
hence x in union (UNION (F,G)) by ; :: thesis: verum
end;
suppose A8: x in union G ; :: thesis: x in union (UNION (F,G))
consider W being object such that
A9: W in F by ;
consider Y being set such that
A10: x in Y and
A11: Y in G by ;
reconsider Y = Y, W = W as set by TARSKI:1;
set YW = W \/ Y;
( Y c= W \/ Y & W \/ Y in UNION (F,G) ) by ;
hence x in union (UNION (F,G)) by ; :: thesis: verum
end;
end;
end;
thus union (UNION (F,G)) c= () \/ () by Th27; :: thesis: verum