set B0 = the Basis of x;
defpred S₁[ Ordinal] means ex B being Basis of x st $1 = card B;
card the Basis of x is ordinal ;
then A1: ex A being Ordinal st S₁[A] ;
consider A being Ordinal such that
A2: S₁[A] and
A3: for B being Ordinal st S₁[B] holds
A c= B from ORDINAL1:sch 1(A1);
consider B1 being Basis of x such that
A4: A = card B1 by A2;
take card B1 ; :: thesis: ( ex B being Basis of x st card B1 = card B & ( for B being Basis of x holds card B1 c= card B ) )
thus ( ex B being Basis of x st card B1 = card B & ( for B being Basis of x holds card B1 c= card B ) ) by A3, A4; :: thesis: verum