let T be TopStruct ; :: thesis: ex b being Basis of T st card b = weight T

defpred S_{1}[ 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 S_{1}[A]

A2: S_{1}[A]
and

A3: for C being Ordinal st S_{1}[C] holds

A c= C from ORDINAL1:sch 1(A1);

consider b being Basis of T such that

A4: A = card b by A2;

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 A4, A5, SETFAM_1:def 1; :: thesis: verum

defpred S

set X = { (card b1) where b1 is Basis of T : verum } ;

A1: ex A being Ordinal st S

proof

consider A being Ordinal such that
take
card the topology of T
; :: thesis: S_{1}[ card the topology of T]

the topology of T is Basis of T by CANTOR_1:2;

hence S_{1}[ card the topology of T]
; :: thesis: verum

end;the topology of T is Basis of T by CANTOR_1:2;

hence S

A2: S

A3: for C being Ordinal st S

A c= C from ORDINAL1:sch 1(A1);

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 ) )

take
b
; :: thesis: card b = weight T( ( ( 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;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

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 A4, A5, SETFAM_1:def 1; :: thesis: verum