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

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