defpred S₁[ Ordinal] means ex M being Cardinal st
( $1 = M & card X in M );
card X in card (bool X) by Th13;
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 M being Cardinal such that
A4: A = M and
A5: card X in M by A2;
take M ; :: thesis: ( card X in M & ( for M being Cardinal st card X in M holds
M c= M ) )
thus card X in M by A5; :: thesis: for M being Cardinal st card X in M holds
M c= M
let N be Cardinal; :: thesis: ( card X in N implies M c= N )
assume card X in N ; :: thesis: M c= N
hence M c= N by A3, A4; :: thesis: verum