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

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