let X be set ; :: thesis: ( X is epsilon-transitive & X is FamUnion-closed implies X is union-closed )

assume A1: ( X is epsilon-transitive & X is FamUnion-closed ) ; :: thesis: X is union-closed

let A be set ; :: according to CLASSES3:def 2 :: thesis: ( A in X implies union A in X )

assume A2: A in X ; :: thesis: union A in X

( dom (id A) = A & rng (id A) = A & A c= X ) by A1, A2;

hence union A in X by A1, A2; :: thesis: verum

assume A1: ( X is epsilon-transitive & X is FamUnion-closed ) ; :: thesis: X is union-closed

let A be set ; :: according to CLASSES3:def 2 :: thesis: ( A in X implies union A in X )

assume A2: A in X ; :: thesis: union A in X

( dom (id A) = A & rng (id A) = A & A c= X ) by A1, A2;

hence union A in X by A1, A2; :: thesis: verum