let T be TopStruct ; :: thesis: ex b being Basis of T st card b = weight T
defpred S1[ Ordinal] means \$1 in { (card b) where b is Basis of T : verum } ;
set X = { (card b1) where b1 is Basis of T : verum } ;
A1: ex A being Ordinal st S1[A]
proof
take card the topology of T ; :: thesis: S1[ card the topology of T]
the topology of T is Basis of T by CANTOR_1:2;
hence S1[ card the topology of T] ; :: thesis: verum
end;
consider A being Ordinal such that
A2: S1[A] and
A3: for C being Ordinal st S1[C] holds
A c= C from consider b being Basis of T such that
A4: A = card b by A2;
A5: 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 A6: 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 A7: y in { (card b1) where b1 is Basis of T : verum } ; :: thesis: x in y
then ex B2 being Basis of T st y = card B2 ;
then reconsider y1 = y as Cardinal ;
A c= y1 by A3, A7;
hence x in y by A6; :: thesis: verum
end;
take b ; :: thesis:
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 card b = weight T by ; :: thesis: verum