let T be T_0 TopSpace; ( T is infinite implies for B being Basis of T holds B is infinite )
assume A1:
T is infinite
; for B being Basis of T holds B is infinite
let B be Basis of T; B is infinite
assume
B is finite
; 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;
hence
contradiction
; verum