set X = { (card B1) where B1 is Basis of T : verum } ;
defpred S₁[ Ordinal] means $1 in { (card B) where B is Basis of T : verum } ;
A1: ex A being Ordinal st S₁[A]

proof

take card the topology of T ; :: thesis: S₁[ card the topology of T]
the topology of T is Basis of T by CANTOR_1:2;
hence S₁[ card the topology of T] ; :: thesis: verum

end;

consider A being Ordinal such that
A2: S₁[A] and
A3: for C being Ordinal st S₁[C] holds
A c= C from ORDINAL1:sch 1(A1);
ex B being Basis of T st A = card B by A2;
then reconsider A = A as Cardinal ;

A4: now :: thesis: for x being object holds
( ( ( for y being set st y in { (card B1) where B1 is Basis of T : verum } holds
x in y ) implies x in A ) & ( x in A implies for y being set st y in { (card B1) where B1 is Basis of T : verum } holds
x in y ) )

let x be object ; :: thesis: ( ( ( for y being set st y in { (card B1) where B1 is Basis of T : verum } holds
x in y ) implies x in A ) & ( x in A implies for y being set st y in { (card B1) where B1 is Basis of T : verum } holds
x in y ) )
thus ( ( for y being set st y in { (card B1) where B1 is Basis of T : verum } holds
x in y ) implies x in A ) by A2; :: thesis: ( x in A implies for y being set st y in { (card B1) where B1 is Basis of T : verum } holds
x in y )
assume A5: x in A ; :: thesis: for y being set st y in { (card B1) where B1 is Basis of T : verum } holds
x in y
let y be set ; :: thesis: ( y in { (card B1) where B1 is Basis of T : verum } implies x in y )
assume A6: y in { (card B1) where B1 is Basis of T : verum } ; :: thesis: x in y
then ex B1 being Basis of T st y = card B1 ;
then reconsider y1 = y as Cardinal ;
A c= y1 by A3, A6;
hence x in y by A5; :: thesis: verum

end;

the topology of T is Basis of T by CANTOR_1:2;
then card the topology of T in { (card B1) where B1 is Basis of T : verum } ;
hence meet { (card B) where B is Basis of T : verum } is Cardinal by A4, SETFAM_1:def 1; :: thesis: verum