let A, B be set ; :: thesis: union (A \/ B) = (union A) \/ (union B)
A1: union (A \/ B) c= (union A) \/ (union B)

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in union (A \/ B) or x in (union A) \/ (union B) )
assume x in union (A \/ B) ; :: thesis: x in (union A) \/ (union B)
then consider Y being set such that
A2: x in Y and
A3: Y in A \/ B by TARSKI:def 4;
( Y in A or Y in B ) by A3, XBOOLE_0:def 3;
then ( x in union A or x in union B ) by A2, TARSKI:def 4;
hence x in (union A) \/ (union B) by XBOOLE_0:def 3; :: thesis: verum

end;

( union A c= union (A \/ B) & union B c= union (A \/ B) ) by Th76, XBOOLE_1:7;
hence union (A \/ B) = (union A) \/ (union B) by A1, XBOOLE_1:8; :: thesis: verum