let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (A _\/_ B) _/\_ (A _\/_ C) or x in A _\/_ (B _/\_ C) )
assume x in (A _\/_ B) _/\_ (A _\/_ C) ; :: thesis: x in A _\/_ (B _/\_ C)
then consider X, Y being set such that
A2: ( X in UNION (A,B) & Y in UNION (A,C) & x = X /\ Y ) by SETFAM_1:def 5;
A3: ( A is non empty ordered Subset-Family of U & B is non empty ordered Subset-Family of U & C is non empty ordered Subset-Family of U ) by Lm4;
x in INTERSECTION ((UNION (A,B)),(UNION (A,C))) by A2, SETFAM_1:def 5;
hence x in A _\/_ (B _/\_ C) by Th29, A3; :: thesis: verum