let T be non empty TopSpace; :: thesis: for x, y being Element of (InclPoset the topology of T) st ex Z being Subset of T st
( x c= Z & Z c= y & Z is compact ) holds
x << y
set L = InclPoset the topology of T;
let x, y be Element of (InclPoset the topology of T); :: thesis: ( ex Z being Subset of T st
( x c= Z & Z c= y & Z is compact ) implies x << y )
given Z being Subset of T such that A1: x c= Z and
A2: Z c= y and
A3: Z is compact ; :: thesis: x << y
A4: InclPoset the topology of T = RelStr(# the topology of T,(RelIncl the topology of T) #) by YELLOW_1:def 1;
then A5: x in the topology of T ;
y in the topology of T by A4;
then reconsider X = x, Y = y as Subset of T by A5;
let D be non empty directed Subset of (InclPoset the topology of T); :: according to WAYBEL_3:def 1 :: thesis: ( y <= sup D implies ex d being Element of (InclPoset the topology of T) st
( d in D & x <= d ) )
A6: sup D = union D by YELLOW_1:22;
reconsider F = D as Subset-Family of T by A4, XBOOLE_1:1;
reconsider F = F as Subset-Family of T ;
A7: F is open
proof
let a be Subset of T; :: according to TOPS_2:def 1 :: thesis: ( not a in F or a is open )
assume a in F ; :: thesis: a is open
hence a in the topology of T by A4; :: according to PRE_TOPC:def 2 :: thesis: verum
end;
assume y <= sup D ; :: thesis: ex d being Element of (InclPoset the topology of T) st
( d in D & x <= d )
then Y c= union F by A6, YELLOW_1:3;
then Z c= union F by A2;
then F is Cover of Z by SETFAM_1:def 11;
then consider G being Subset-Family of T such that
A8: G c= F and
A9: G is Cover of Z and
A10: G is finite by A3, A7;
consider d being Element of (InclPoset the topology of T) such that
A11: d in D and
A12: d is_>=_than G by A8, A10, WAYBEL_0:1;
take d ; :: thesis: ( d in D & x <= d )
thus d in D by A11; :: thesis: x <= d
A13: now :: thesis: for B being set st B in G holds
B c= d
let B be set ; :: thesis: ( B in G implies B c= d )
assume A14: B in G ; :: thesis: B c= d
then B in D by A8;
then reconsider e = B as Element of (InclPoset the topology of T) ;
d >= e by A12, A14;
hence B c= d by YELLOW_1:3; :: thesis: verum
end;
A15: Z c= union G by A9, SETFAM_1:def 11;
union G c= d by A13, ZFMISC_1:76;
then Z c= d by A15;
then X c= d by A1;
hence x <= d by YELLOW_1:3; :: thesis: verum