let T be T_0 TopSpace; :: thesis: ( not T is finite implies for B being Basis of T holds not B is finite )
assume A1: not T is finite ; :: thesis: for B being Basis of T holds not B is finite
let B be Basis of T; :: thesis: not B is finite
assume B is finite ; :: thesis: contradiction
then reconsider B1 = B as finite Subset-Family of T ;
union (Components B1) = the carrier of T by Th19;
then consider X being set such that
A2: X in Components B1 and
A3: not X is finite by A1, FINSET_1:25;
reconsider X = X as infinite set by A3;
consider x being set such that
A4: x in X by XBOOLE_0:def 1;
consider y being set such that
A5: y in X and
A6: x <> y by A4, Th4;
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

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 Y meets X by XBOOLE_0:4;
then X c= Y by A2, A7, Th30;
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 Y meets X by XBOOLE_0:4;
then X c= Y by A2, A7, Th30;
hence contradiction by A4, A10; :: thesis: verum

end;

end;

end;

hence contradiction ; :: thesis: verum