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