let T be non empty TopSpace; :: thesis: for J being Basis of T holds not J is empty
let J be Basis of T; :: thesis: not J is empty
assume J is empty ; :: thesis: contradiction
then A1: UniCl J = {{}} by YELLOW_9:16;
( the topology of T c= UniCl J & the carrier of T in the topology of T ) by CANTOR_1:def 2, PRE_TOPC:def 1;
hence contradiction by A1, TARSKI:def 1; :: thesis: verum