let T be TopStruct ; :: thesis: for B being Basis of T
for S being Subset of T st S in B holds
S is open
let B be Basis of T; :: thesis: for S being Subset of T st S in B holds
S is open
let S be Subset of T; :: thesis: ( S in B implies S is open )
assume A1: S in B ; :: thesis: S is open
B c= the topology of T by TOPS_2:64;
hence S is open by A1; :: thesis: verum