let T be non empty TopSpace; :: thesis: ( T is locally-compact implies InclPoset the topology of T is continuous )
assume A1: T is locally-compact ; :: thesis: InclPoset the topology of T is continuous
set L = InclPoset the topology of T;
A2: InclPoset the topology of T = RelStr(# the topology of T,(RelIncl the topology of T) #) by YELLOW_1:def 1;
thus for x being Element of (InclPoset the topology of T) holds
( not waybelow x is empty & waybelow x is directed ) ; :: according to WAYBEL_3:def 6 :: thesis: ( InclPoset the topology of T is up-complete & InclPoset the topology of T is satisfying_axiom_of_approximation )
thus InclPoset the topology of T is up-complete ; :: thesis: InclPoset the topology of T is satisfying_axiom_of_approximation
let x be Element of (InclPoset the topology of T); :: according to WAYBEL_3:def 5 :: thesis: x = sup (waybelow x)
x in the topology of T by A2;
then reconsider X = x as Subset of T ;
thus x c= sup (waybelow x) :: according to XBOOLE_0:def 10 :: thesis: sup (waybelow x) c= x

proof

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in x or a in sup (waybelow x) )
assume A3: a in x ; :: thesis: a in sup (waybelow x)
X is open by A2;
then consider Y being Subset of T such that
A4: a in Int Y and
A5: Y c= X and
A6: Y is compact by A1, A3;
reconsider iY = Int Y as Subset of T ;
reconsider y = iY as Element of (InclPoset the topology of T) by A2, PRE_TOPC:def 2;
y << x by A5, A6, Th38, TOPS_1:16;
then y in waybelow x ;
then y c= union (waybelow x) by ZFMISC_1:74;
then y c= sup (waybelow x) by YELLOW_1:22;
hence a in sup (waybelow x) by A4; :: thesis: verum

end;

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in sup (waybelow x) or a in x )
assume a in sup (waybelow x) ; :: thesis: a in x
then a in union (waybelow x) by YELLOW_1:22;
then consider Y being set such that
A7: a in Y and
A8: Y in waybelow x by TARSKI:def 4;
consider y being Element of (InclPoset the topology of T) such that
A9: Y = y and
A10: y << x by A8;
y <= x by A10, Th1;
then Y c= x by A9, YELLOW_1:3;
hence a in x by A7; :: thesis: verum