let X be set ; :: thesis: ( X is epsilon-transitive & X is Tarski implies ( X is union-closed & X is FamUnion-closed ) )
assume A1: ( X is epsilon-transitive & X is Tarski ) ; :: thesis: ( X is union-closed & X is FamUnion-closed )
thus X is union-closed by A1, CLASSES2:59; :: thesis: X is FamUnion-closed
let Y be set ; :: according to CLASSES3:def 3 :: thesis: for f being Function st dom f = Y & rng f c= X & Y in X holds
union (rng f) in X
let f be Function; :: thesis: ( dom f = Y & rng f c= X & Y in X implies union (rng f) in X )
assume A2: ( dom f = Y & rng f c= X & Y in X ) ; :: thesis: union (rng f) in X
reconsider X = X as Universe by A1, A2;
( not Y,X are_equipotent & card Y in card X ) by A2, CLASSES2:1;
then card (rng f) in card X by A2, ORDINAL1:12, CARD_1:12;
then A3: card (rng f) <> card X ;
( rng f,X are_equipotent or rng f in X ) by A2, CLASSES1:def 2;
hence union (rng f) in X by A3, CARD_1:5, CLASSES2:59; :: thesis: verum