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