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;

now :: thesis: contradiction

per cases ( ( x in Y & not y in Y ) or ( y in Y & not x in Y ) ) by A8;

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;

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;

end;

end;

hence contradiction ; :: thesis: verum