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