set B0 = [#] T;
defpred S₁[ Ordinal] means ex A being Subset of T st
( A is dense & $1 = card A );
card ([#] T) 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 Subset of T such that
A4: ( B1 is dense & A = card B1 ) by A2;
take card B1 ; :: thesis: ( ex A being Subset of T st
( A is dense & card B1 = card A ) & ( for B being Subset of T st B is dense holds
card B1 c= card B ) )
thus ( ex A being Subset of T st
( A is dense & card B1 = card A ) & ( for B being Subset of T st B is dense holds
card B1 c= card B ) ) by A3, A4; :: thesis: verum