let T be non empty TopSpace; :: thesis: for x, y being Element of (InclPoset the topology of T) st ( 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 ) holds
x is_way_below y
set L = InclPoset the topology of T;
A1: InclPoset the topology of T = RelStr(# the topology of T,(RelIncl the topology of T) #) by YELLOW_1:def 1;
let x, y be Element of (InclPoset the topology of T); :: 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 ) implies x is_way_below y )
assume A2: 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 ; :: thesis: x is_way_below y
now :: thesis: for I being Ideal of (InclPoset the topology of T) st y <= sup I holds
x in I
let I be Ideal of (InclPoset the topology of T); :: thesis: ( y <= sup I implies x in I )
reconsider F = I as Subset-Family of T by A1, XBOOLE_1:1;
assume y <= sup I ; :: thesis: x in I
then y c= sup I by YELLOW_1:3;
then A3: y c= union F by YELLOW_1:22;
F is open by YELLOW_1:25;
then consider G being finite Subset of F such that
A4: x c= union G by A2, A3;
reconsider G = G as finite Subset of (InclPoset the topology of T) by XBOOLE_1:1;
consider z being Element of (InclPoset the topology of T) such that
A5: z in I and
A6: z is_>=_than G by WAYBEL_0:1;
A7: union G = sup G by YELLOW_1:22;
A8: z >= sup G by A6, YELLOW_0:32;
A9: x <= sup G by A4, A7, YELLOW_1:3;
sup G in I by A5, A8, WAYBEL_0:def 19;
hence x in I by A9, WAYBEL_0:def 19; :: thesis: verum
end;
hence x is_way_below y by Th21; :: thesis: verum