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

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

then X is Tarski by Th17;

hence X is universal by A1; :: thesis: verum

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

then X is Tarski by Th17;

hence X is universal by A1; :: thesis: verum