ex A being Ordinal st
( P₁[A] & ( for B being Ordinal st P₁[B] holds
A c= B ) )

A1: ex A being Ordinal st P₁[A]