let T be non empty TopStruct ; :: thesis: for B being Basis of T
for V being Subset of T st V is open & V <> {} holds
ex W being Subset of T st
( W in B & W c= V & W <> {} )
let B be Basis of T; :: thesis: for V being Subset of T st V is open & V <> {} holds
ex W being Subset of T st
( W in B & W c= V & W <> {} )
let V be Subset of T; :: thesis: ( V is open & V <> {} implies ex W being Subset of T st
( W in B & W c= V & W <> {} ) )
assume A1: ( V is open & V <> {} ) ; :: thesis: ex W being Subset of T st
( W in B & W c= V & W <> {} )
then A2: V = union { G where G is Subset of T : ( G in B & G c= V ) } by YELLOW_8:18;
consider x being set such that
A3: x in V by A1, XBOOLE_0:def 1;
consider Y being set such that
A4: ( x in Y & Y in { G where G is Subset of T : ( G in B & G c= V ) } ) by A2, A3, TARSKI:def 4;
consider Z being Subset of T such that
A5: ( Z = Y & Z in B & Z c= V ) by A4;
thus ex W being Subset of T st
( W in B & W c= V & W <> {} ) by A4, A5; :: thesis: verum