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 ;
A2: not the carrier of T is finite by A1;
union (Components B1) = the carrier of T by Th19;
then consider X being set such that
A3: X in Components B1 and
A4: not X is finite by A2, FINSET_1:25;
reconsider X = X as infinite set by A4;
consider x being set such that
A5: x in X by XBOOLE_0:def 1;
consider y being set such that
A6: y in X and
A7: x <> y by A5, Th4;
reconsider x1 = x, y1 = y as Element of T by A3, A5, A6;
not the carrier of T is empty by A1;
then not T is empty ;
then consider Y being Subset of T such that
A8: Y is open and
A9: ( ( x1 in Y & not y1 in Y ) or ( y1 in Y & not x1 in Y ) ) by A7, T_0TOPSP:def 7;

now

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

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

then x in Y /\ X by A5, XBOOLE_0:def 4;
then Y meets X by XBOOLE_0:4;
then X c= Y by A3, A8, Th30;
hence contradiction by A6, A10; :: thesis: verum

end;

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

then y in Y /\ X by A6, XBOOLE_0:def 4;
then Y meets X by XBOOLE_0:4;
then X c= Y by A3, A8, Th30;
hence contradiction by A5, A11; :: thesis: verum

end;

end;

end;

hence contradiction ; :: thesis: verum