let T be non empty TopSpace; :: thesis: for x, y being Element of (InclPoset the topology of T) st x is_way_below y holds
for F being Subset-Family of T st F is open & y c= union F holds
ex G being finite Subset of F st x c= union G
set L = InclPoset the topology of T;
let x, y be Element of (InclPoset the topology of T); :: thesis: ( x is_way_below y implies for F being Subset-Family of T st F is open & y c= union F holds
ex G being finite Subset of F st x c= union G )
assume A1: x << y ; :: thesis: for F being Subset-Family of T st F is open & y c= union F holds
ex G being finite Subset of F st x c= union G
let F be Subset-Family of T; :: thesis: ( F is open & y c= union F implies ex G being finite Subset of F st x c= union G )
assume that
A2: F is open and
A3: y c= union F ; :: thesis: ex G being finite Subset of F st x c= union G
reconsider A = F as Subset of (InclPoset the topology of T) by A2, YELLOW_1:25;
sup A = union F by YELLOW_1:22;
then y <= sup A by A3, YELLOW_1:3;
then consider B being finite Subset of (InclPoset the topology of T) such that
A4: B c= A and
A5: x <= sup B by A1, Th18;
reconsider G = B as finite Subset of F by A4;
take G ; :: thesis: x c= union G
sup B = union G by YELLOW_1:22;
hence x c= union G by A5, YELLOW_1:3; :: thesis: verum