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 () = the carrier of T by Th15;
then consider X being set such that
A2: X in Components B1 and
A3: X is infinite by ;
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 ;
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 ;
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
end;
suppose A10: ( y in Y & not x in Y ) ; :: thesis: contradiction
end;
end;
end;
hence contradiction ; :: thesis: verum