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 that

A1: V is open and

A2: V <> {} ; :: thesis: ex W being Subset of T st

( W in B & W c= V & W <> {} )

consider x being object such that

A3: x in V by A2, XBOOLE_0:def 1;

V = union { G where G is Subset of T : ( G in B & G c= V ) } by A1, YELLOW_8:9;

then consider Y being set such that

A4: x in Y and

A5: Y in { G where G is Subset of T : ( G in B & G c= V ) } by A3, TARSKI:def 4;

ex Z being Subset of T st

( Z = Y & Z in B & Z c= V ) by A5;

hence ex W being Subset of T st

( W in B & W c= V & W <> {} ) by A4; :: thesis: verum

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 that

A1: V is open and

A2: V <> {} ; :: thesis: ex W being Subset of T st

( W in B & W c= V & W <> {} )

consider x being object such that

A3: x in V by A2, XBOOLE_0:def 1;

V = union { G where G is Subset of T : ( G in B & G c= V ) } by A1, YELLOW_8:9;

then consider Y being set such that

A4: x in Y and

A5: Y in { G where G is Subset of T : ( G in B & G c= V ) } by A3, TARSKI:def 4;

ex Z being Subset of T st

( Z = Y & Z in B & Z c= V ) by A5;

hence ex W being Subset of T st

( W in B & W c= V & W <> {} ) by A4; :: thesis: verum