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 & Z c= y & Z is compact ) ; :: thesis: x << y
A2: InclPoset the topology of T = RelStr(# the topology of T,(RelIncl the topology of T) #) by YELLOW_1:def 1;
then ( x in the topology of T & y in the topology of T ) ;
then reconsider X = x, Y = y as Subset of T ;
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 ) )
A3: sup D = union D by YELLOW_1:22;
reconsider F = D as Subset-Family of T by A2, XBOOLE_1:1;
reconsider F = F as Subset-Family of T ;
A4: 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 A2; :: according to PRE_TOPC:def 5 :: 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 A3, YELLOW_1:3;
then Z c= union F by A1, XBOOLE_1:1;
then F is Cover of Z by SETFAM_1:def 12;
then consider G being Subset-Family of T such that
A5: ( G c= F & G is Cover of Z & G is finite ) by A1, A4, COMPTS_1:def 7;
consider d being Element of (InclPoset the topology of T) such that
A6: ( d in D & d is_>=_than G ) by A5, WAYBEL_0:1;
take d ; :: thesis: ( d in D & x <= d )
thus d in D by A6; :: thesis: x <= d

now

let B be set ; :: thesis: ( B in G implies B c= d )
assume A7: B in G ; :: thesis: B c= d
then B in D by A5;
then reconsider e = B as Element of (InclPoset the topology of T) ;
d >= e by A6, A7, LATTICE3:def 9;
hence B c= d by YELLOW_1:3; :: thesis: verum

end;

then ( Z c= union G & union G c= d ) by A5, SETFAM_1:def 12, ZFMISC_1:94;
then Z c= d by XBOOLE_1:1;
then X c= d by A1, XBOOLE_1:1;
hence x <= d by YELLOW_1:3; :: thesis: verum