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 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