let T be TopSpace; :: thesis: for K being Basis of T holds
( K is open & K is prebasis of T )
let K be Basis of T; :: thesis: ( K is open & K is prebasis of T )
K c= the topology of T by CANTOR_1:def 2;
hence for P being Subset of T st P in K holds
P is open by PRE_TOPC:def 5; :: according to TOPS_2:def 1 :: thesis: K is prebasis of T
thus K c= the topology of T by CANTOR_1:def 2; :: according to CANTOR_1:def 5 :: thesis: ex b₁ being Basis of T st b₁ c= FinMeetCl K
take K ; :: thesis: K c= FinMeetCl K
thus K c= FinMeetCl K by CANTOR_1:4; :: thesis: verum