consider B0 being Basis of x;
defpred S₁[ ordinal number ] means ex B being Basis of x st $1 = card B;
card B0 is ordinal ;
then A1: ex A being ordinal number st S₁[A] ;
consider A being ordinal number such that
A2: S₁[A] and
A3: for B being ordinal number 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