let T be T_0 TopSpace; :: thesis: ( T is infinite implies for B being Basis of T holds B is infinite )

assume A1: T is infinite ; :: thesis: for B being Basis of T holds B is infinite

let B be Basis of T; :: thesis: B is infinite

assume B is finite ; :: thesis: contradiction

then reconsider B1 = B as finite Subset-Family of T ;

union (Components B1) = the carrier of T by Th15;

then consider X being set such that

A2: X in Components B1 and

A3: X is infinite by A1, FINSET_1:7;

reconsider X = X as infinite set by A3;

consider x being object such that

A4: x in X by XBOOLE_0:def 1;

consider y being object such that

A5: y in X and

A6: x <> y by A4, SUBSET_1:48;

reconsider x1 = x, y1 = y as Element of T by A2, A4, A5;

consider Y being Subset of T such that

A7: Y is open and

A8: ( ( x1 in Y & not y1 in Y ) or ( y1 in Y & not x1 in Y ) ) by A1, A6, T_0TOPSP:def 7;

assume A1: T is infinite ; :: thesis: for B being Basis of T holds B is infinite

let B be Basis of T; :: thesis: B is infinite

assume B is finite ; :: thesis: contradiction

then reconsider B1 = B as finite Subset-Family of T ;

union (Components B1) = the carrier of T by Th15;

then consider X being set such that

A2: X in Components B1 and

A3: X is infinite by A1, FINSET_1:7;

reconsider X = X as infinite set by A3;

consider x being object such that

A4: x in X by XBOOLE_0:def 1;

consider y being object such that

A5: y in X and

A6: x <> y by A4, SUBSET_1:48;

reconsider x1 = x, y1 = y as Element of T by A2, A4, A5;

consider Y being Subset of T such that

A7: Y is open and

A8: ( ( x1 in Y & not y1 in Y ) or ( y1 in Y & not x1 in Y ) ) by A1, A6, T_0TOPSP:def 7;

now :: thesis: contradictionend;

hence
contradiction
; :: thesis: verumper cases
( ( x in Y & not y in Y ) or ( y in Y & not x in Y ) )
by A8;

end;

suppose A9:
( x in Y & not y in Y )
; :: thesis: contradiction

then
x in Y /\ X
by A4, XBOOLE_0:def 4;

then X c= Y by A2, A7, Th26, XBOOLE_0:4;

hence contradiction by A5, A9; :: thesis: verum

end;then X c= Y by A2, A7, Th26, XBOOLE_0:4;

hence contradiction by A5, A9; :: thesis: verum

suppose A10:
( y in Y & not x in Y )
; :: thesis: contradiction

then
y in Y /\ X
by A5, XBOOLE_0:def 4;

then X c= Y by A2, A7, Th26, XBOOLE_0:4;

hence contradiction by A4, A10; :: thesis: verum

end;then X c= Y by A2, A7, Th26, XBOOLE_0:4;

hence contradiction by A4, A10; :: thesis: verum