let T be TopSpace; :: thesis: for K being prebasis of T holds K is open
let K be prebasis of T; :: thesis: K is open
let P be Subset of T; :: according to TOPS_2:def 1 :: thesis: ( not P in K or P is open )
A1: K c= the topology of T by CANTOR_1:def 5;
assume P in K ; :: thesis: P is open
hence P in the topology of T by A1; :: according to PRE_TOPC:def 5 :: thesis: verum