:: by Grzegorz Bancerek

::

:: Received October 11, 1996

:: Copyright (c) 1996-2021 Association of Mizar Users

:: deftheorem defines is_way_below WAYBEL_3:def 1 :

for L being non empty reflexive RelStr

for x, y being Element of L holds

( x is_way_below y iff for D being non empty directed Subset of L st y <= sup D holds

ex d being Element of L st

( d in D & x <= d ) );

for L being non empty reflexive RelStr

for x, y being Element of L holds

( x is_way_below y iff for D being non empty directed Subset of L st y <= sup D holds

ex d being Element of L st

( d in D & x <= d ) );

notation

let L be non empty reflexive RelStr ;

let x, y be Element of L;

synonym x << y for x is_way_below y;

synonym y >> x for x is_way_below y;

end;
let x, y be Element of L;

synonym x << y for x is_way_below y;

synonym y >> x for x is_way_below y;

:: deftheorem defines compact WAYBEL_3:def 2 :

for L being non empty reflexive RelStr

for x being Element of L holds

( x is compact iff x is_way_below x );

for L being non empty reflexive RelStr

for x being Element of L holds

( x is compact iff x is_way_below x );

notation

let L be non empty reflexive RelStr ;

let x be Element of L;

synonym isolated_from_below x for compact ;

end;
let x be Element of L;

synonym isolated_from_below x for compact ;

theorem Th1: :: WAYBEL_3:1

for L being non empty reflexive antisymmetric RelStr

for x, y being Element of L st x << y holds

x <= y

for x, y being Element of L st x << y holds

x <= y

proof end;

theorem Th2: :: WAYBEL_3:2

for L being non empty reflexive transitive RelStr

for u, x, y, z being Element of L st u <= x & x << y & y <= z holds

u << z

for u, x, y, z being Element of L st u <= x & x << y & y <= z holds

u << z

proof end;

theorem Th3: :: WAYBEL_3:3

for L being non empty Poset st ( L is with_suprema or L is /\-complete ) holds

for x, y, z being Element of L st x << z & y << z holds

( ex_sup_of {x,y},L & x "\/" y << z )

for x, y, z being Element of L st x << z & y << z holds

( ex_sup_of {x,y},L & x "\/" y << z )

proof end;

theorem Th4: :: WAYBEL_3:4

for L being non empty reflexive antisymmetric lower-bounded RelStr

for x being Element of L holds Bottom L << x

for x being Element of L holds Bottom L << x

proof end;

theorem :: WAYBEL_3:6

for L being non empty reflexive antisymmetric RelStr

for x, y being Element of L st x << y & x >> y holds

x = y

for x, y being Element of L st x << y & x >> y holds

x = y

proof end;

definition

let L be non empty reflexive RelStr ;

let x be Element of L;

A1: { y where y is Element of L : y << x } c= the carrier of L

coherence

{ y where y is Element of L : y << x } is Subset of L;

by A1;

A2: { y where y is Element of L : y >> x } c= the carrier of L

coherence

{ y where y is Element of L : y >> x } is Subset of L;

by A2;

end;
let x be Element of L;

A1: { y where y is Element of L : y << x } c= the carrier of L

proof end;

correctness coherence

{ y where y is Element of L : y << x } is Subset of L;

by A1;

A2: { y where y is Element of L : y >> x } c= the carrier of L

proof end;

correctness coherence

{ y where y is Element of L : y >> x } is Subset of L;

by A2;

:: deftheorem defines waybelow WAYBEL_3:def 3 :

for L being non empty reflexive RelStr

for x being Element of L holds waybelow x = { y where y is Element of L : y << x } ;

for L being non empty reflexive RelStr

for x being Element of L holds waybelow x = { y where y is Element of L : y << x } ;

:: deftheorem defines wayabove WAYBEL_3:def 4 :

for L being non empty reflexive RelStr

for x being Element of L holds wayabove x = { y where y is Element of L : y >> x } ;

for L being non empty reflexive RelStr

for x being Element of L holds wayabove x = { y where y is Element of L : y >> x } ;

theorem Th7: :: WAYBEL_3:7

for L being non empty reflexive RelStr

for x, y being Element of L holds

( x in waybelow y iff x << y )

for x, y being Element of L holds

( x in waybelow y iff x << y )

proof end;

theorem Th8: :: WAYBEL_3:8

for L being non empty reflexive RelStr

for x, y being Element of L holds

( x in wayabove y iff x >> y )

for x, y being Element of L holds

( x in wayabove y iff x >> y )

proof end;

theorem Th9: :: WAYBEL_3:9

for L being non empty reflexive antisymmetric RelStr

for x being Element of L holds x is_>=_than waybelow x by Th7, Th1;

for x being Element of L holds x is_>=_than waybelow x by Th7, Th1;

theorem :: WAYBEL_3:10

for L being non empty reflexive antisymmetric RelStr

for x being Element of L holds x is_<=_than wayabove x by Th8, Th1;

for x being Element of L holds x is_<=_than wayabove x by Th8, Th1;

theorem Th11: :: WAYBEL_3:11

for L being non empty reflexive antisymmetric RelStr

for x being Element of L holds

( waybelow x c= downarrow x & wayabove x c= uparrow x )

for x being Element of L holds

( waybelow x c= downarrow x & wayabove x c= uparrow x )

proof end;

theorem Th12: :: WAYBEL_3:12

for L being non empty reflexive transitive RelStr

for x, y being Element of L st x <= y holds

( waybelow x c= waybelow y & wayabove y c= wayabove x )

for x, y being Element of L st x <= y holds

( waybelow x c= waybelow y & wayabove y c= wayabove x )

proof end;

registration

let L be non empty reflexive antisymmetric lower-bounded RelStr ;

let x be Element of L;

coherence

not waybelow x is empty

end;
let x be Element of L;

coherence

not waybelow x is empty

proof end;

registration

let L be non empty reflexive transitive RelStr ;

let x be Element of L;

coherence

waybelow x is lower

wayabove x is upper

end;
let x be Element of L;

coherence

waybelow x is lower

proof end;

coherence wayabove x is upper

proof end;

registration
end;

registration

let L be non empty /\-complete Poset;

let x be Element of L;

coherence

waybelow x is directed

end;
let x be Element of L;

coherence

waybelow x is directed

proof end;

:: EXAMPLES, 1.3, p. 39

registration

let L be non empty connected RelStr ;

coherence

for b_{1} being Subset of L holds

( b_{1} is directed & b_{1} is filtered )

end;
coherence

for b

( b

proof end;

registration

for b_{1} being Chain st b_{1} is up-complete & b_{1} is lower-bounded holds

b_{1} is complete
end;

cluster non empty reflexive transitive antisymmetric lower-bounded connected up-complete -> complete for RelStr ;

coherence for b

b

proof end;

theorem :: WAYBEL_3:14

theorem :: WAYBEL_3:15

for L being non empty reflexive antisymmetric lower-bounded RelStr holds Bottom L is compact by Th4;

theorem Th16: :: WAYBEL_3:16

for L being non empty up-complete Poset

for D being non empty finite directed Subset of L holds sup D in D

for D being non empty finite directed Subset of L holds sup D in D

proof end;

theorem :: WAYBEL_3:17

for L being non empty up-complete Poset st L is finite holds

for x being Element of L holds x is isolated_from_below

for x being Element of L holds x is isolated_from_below

proof end;

theorem Th18: :: WAYBEL_3:18

for L being complete LATTICE

for x, y being Element of L st x << y holds

for X being Subset of L st y <= sup X holds

ex A being finite Subset of L st

( A c= X & x <= sup A )

for x, y being Element of L st x << y holds

for X being Subset of L st y <= sup X holds

ex A being finite Subset of L st

( A c= X & x <= sup A )

proof end;

theorem :: WAYBEL_3:19

for L being complete LATTICE

for x, y being Element of L st ( for X being Subset of L st y <= sup X holds

ex A being finite Subset of L st

( A c= X & x <= sup A ) ) holds

x << y

for x, y being Element of L st ( for X being Subset of L st y <= sup X holds

ex A being finite Subset of L st

( A c= X & x <= sup A ) ) holds

x << y

proof end;

theorem :: WAYBEL_3:20

for L being non empty reflexive transitive RelStr

for x, y being Element of L st x << y holds

for I being Ideal of L st y <= sup I holds

x in I

for x, y being Element of L st x << y holds

for I being Ideal of L st y <= sup I holds

x in I

proof end;

theorem Th21: :: WAYBEL_3:21

for L being non empty up-complete Poset

for x, y being Element of L st ( for I being Ideal of L st y <= sup I holds

x in I ) holds

x << y

for x, y being Element of L st ( for I being Ideal of L st y <= sup I holds

x in I ) holds

x << y

proof end;

theorem :: WAYBEL_3:22

for L being lower-bounded LATTICE st L is meet-continuous holds

for x, y being Element of L holds

( x << y iff for I being Ideal of L st y = sup I holds

x in I )

for x, y being Element of L holds

( x << y iff for I being Ideal of L st y = sup I holds

x in I )

proof end;

theorem :: WAYBEL_3:23

for L being complete LATTICE holds

( ( for x being Element of L holds x is compact ) iff for X being non empty Subset of L ex x being Element of L st

( x in X & ( for y being Element of L st y in X holds

not x < y ) ) )

( ( for x being Element of L holds x is compact ) iff for X being non empty Subset of L ex x being Element of L st

( x in X & ( for y being Element of L st y in X holds

not x < y ) ) )

proof end;

definition

let L be non empty reflexive RelStr ;

end;
attr L is satisfying_axiom_of_approximation means :Def5: :: WAYBEL_3:def 5

for x being Element of L holds x = sup (waybelow x);

for x being Element of L holds x = sup (waybelow x);

:: deftheorem Def5 defines satisfying_axiom_of_approximation WAYBEL_3:def 5 :

for L being non empty reflexive RelStr holds

( L is satisfying_axiom_of_approximation iff for x being Element of L holds x = sup (waybelow x) );

for L being non empty reflexive RelStr holds

( L is satisfying_axiom_of_approximation iff for x being Element of L holds x = sup (waybelow x) );

registration

coherence

for b_{1} being 1 -element reflexive RelStr holds b_{1} is satisfying_axiom_of_approximation
by ZFMISC_1:def 10;

end;
for b

definition

let L be non empty reflexive RelStr ;

end;
attr L is continuous means :Def6: :: WAYBEL_3:def 6

( ( for x being Element of L holds

( not waybelow x is empty & waybelow x is directed ) ) & L is up-complete & L is satisfying_axiom_of_approximation );

( ( for x being Element of L holds

( not waybelow x is empty & waybelow x is directed ) ) & L is up-complete & L is satisfying_axiom_of_approximation );

:: deftheorem Def6 defines continuous WAYBEL_3:def 6 :

for L being non empty reflexive RelStr holds

( L is continuous iff ( ( for x being Element of L holds

( not waybelow x is empty & waybelow x is directed ) ) & L is up-complete & L is satisfying_axiom_of_approximation ) );

for L being non empty reflexive RelStr holds

( L is continuous iff ( ( for x being Element of L holds

( not waybelow x is empty & waybelow x is directed ) ) & L is up-complete & L is satisfying_axiom_of_approximation ) );

registration

for b_{1} being non empty reflexive RelStr st b_{1} is continuous holds

( b_{1} is up-complete & b_{1} is satisfying_axiom_of_approximation )
;

for b_{1} being lower-bounded sup-Semilattice st b_{1} is up-complete & b_{1} is satisfying_axiom_of_approximation holds

b_{1} is continuous
;

end;

cluster non empty reflexive continuous -> non empty reflexive up-complete satisfying_axiom_of_approximation for RelStr ;

coherence for b

( b

cluster reflexive transitive antisymmetric lower-bounded with_suprema up-complete satisfying_axiom_of_approximation -> lower-bounded continuous for RelStr ;

coherence for b

b

registration

ex b_{1} being LATTICE st

( b_{1} is continuous & b_{1} is complete & b_{1} is strict )
end;

cluster non empty strict V237() reflexive transitive antisymmetric with_suprema with_infima complete continuous for RelStr ;

existence ex b

( b

proof end;

registration

let L be non empty reflexive continuous RelStr ;

let x be Element of L;

coherence

( not waybelow x is empty & waybelow x is directed ) by Def6;

end;
let x be Element of L;

coherence

( not waybelow x is empty & waybelow x is directed ) by Def6;

theorem :: WAYBEL_3:24

for L being up-complete Semilattice st ( for x being Element of L holds

( not waybelow x is empty & waybelow x is directed ) ) holds

( L is satisfying_axiom_of_approximation iff for x, y being Element of L st not x <= y holds

ex u being Element of L st

( u << x & not u <= y ) )

( not waybelow x is empty & waybelow x is directed ) ) holds

( L is satisfying_axiom_of_approximation iff for x, y being Element of L st not x <= y holds

ex u being Element of L st

( u << x & not u <= y ) )

proof end;

theorem :: WAYBEL_3:25

for L being continuous LATTICE

for x, y being Element of L holds

( x <= y iff waybelow x c= waybelow y )

for x, y being Element of L holds

( x <= y iff waybelow x c= waybelow y )

proof end;

registration

for b_{1} being Chain st b_{1} is complete holds

b_{1} is satisfying_axiom_of_approximation
end;

cluster non empty reflexive transitive antisymmetric complete connected -> satisfying_axiom_of_approximation for RelStr ;

coherence for b

b

proof end;

theorem :: WAYBEL_3:26

for L being complete LATTICE st ( for x being Element of L holds x is compact ) holds

L is satisfying_axiom_of_approximation

L is satisfying_axiom_of_approximation

proof end;

definition

let f be Relation;

end;
attr f is non-Empty means :Def7: :: WAYBEL_3:def 7

for S being 1-sorted st S in rng f holds

not S is empty ;

for S being 1-sorted st S in rng f holds

not S is empty ;

attr f is reflexive-yielding means :Def8: :: WAYBEL_3:def 8

for S being RelStr st S in rng f holds

S is reflexive ;

for S being RelStr st S in rng f holds

S is reflexive ;

:: deftheorem Def7 defines non-Empty WAYBEL_3:def 7 :

for f being Relation holds

( f is non-Empty iff for S being 1-sorted st S in rng f holds

not S is empty );

for f being Relation holds

( f is non-Empty iff for S being 1-sorted st S in rng f holds

not S is empty );

:: deftheorem Def8 defines reflexive-yielding WAYBEL_3:def 8 :

for f being Relation holds

( f is reflexive-yielding iff for S being RelStr st S in rng f holds

S is reflexive );

for f being Relation holds

( f is reflexive-yielding iff for S being RelStr st S in rng f holds

S is reflexive );

registration

let I be set ;

ex b_{1} being ManySortedSet of I st

( b_{1} is RelStr-yielding & b_{1} is non-Empty & b_{1} is reflexive-yielding )

end;
cluster Relation-like I -defined Function-like V34(I) RelStr-yielding non-Empty reflexive-yielding for set ;

existence ex b

( b

proof end;

registration

let I be set ;

let J be RelStr-yielding non-Empty ManySortedSet of I;

coherence

not product J is empty

end;
let J be RelStr-yielding non-Empty ManySortedSet of I;

coherence

not product J is empty

proof end;

definition

let I be non empty set ;

let J be RelStr-yielding ManySortedSet of I;

let i be Element of I;

:: original: .

redefine func J . i -> RelStr ;

coherence

J . i is RelStr

end;
let J be RelStr-yielding ManySortedSet of I;

let i be Element of I;

:: original: .

redefine func J . i -> RelStr ;

coherence

J . i is RelStr

proof end;

registration

let I be non empty set ;

let J be RelStr-yielding non-Empty ManySortedSet of I;

let i be Element of I;

coherence

for b_{1} being RelStr st b_{1} = J . i holds

not b_{1} is empty

end;
let J be RelStr-yielding non-Empty ManySortedSet of I;

let i be Element of I;

coherence

for b

not b

proof end;

registration

let I be set ;

let J be RelStr-yielding non-Empty ManySortedSet of I;

coherence

product J is constituted-Functions

end;
let J be RelStr-yielding non-Empty ManySortedSet of I;

coherence

product J is constituted-Functions

proof end;

definition

let I be non empty set ;

let J be RelStr-yielding non-Empty ManySortedSet of I;

let x be Element of (product J);

let i be Element of I;

:: original: .

redefine func x . i -> Element of (J . i);

coherence

x . i is Element of (J . i)

end;
let J be RelStr-yielding non-Empty ManySortedSet of I;

let x be Element of (product J);

let i be Element of I;

:: original: .

redefine func x . i -> Element of (J . i);

coherence

x . i is Element of (J . i)

proof end;

definition

let I be non empty set ;

let J be RelStr-yielding non-Empty ManySortedSet of I;

let i be Element of I;

let X be Subset of (product J);

:: original: pi

redefine func pi (X,i) -> Subset of (J . i);

coherence

pi (X,i) is Subset of (J . i)

end;
let J be RelStr-yielding non-Empty ManySortedSet of I;

let i be Element of I;

let X be Subset of (product J);

:: original: pi

redefine func pi (X,i) -> Subset of (J . i);

coherence

pi (X,i) is Subset of (J . i)

proof end;

theorem Th27: :: WAYBEL_3:27

for I being non empty set

for J being RelStr-yielding non-Empty ManySortedSet of I

for x being Function holds

( x is Element of (product J) iff ( dom x = I & ( for i being Element of I holds x . i is Element of (J . i) ) ) )

for J being RelStr-yielding non-Empty ManySortedSet of I

for x being Function holds

( x is Element of (product J) iff ( dom x = I & ( for i being Element of I holds x . i is Element of (J . i) ) ) )

proof end;

theorem Th28: :: WAYBEL_3:28

for I being non empty set

for J being RelStr-yielding non-Empty ManySortedSet of I

for x, y being Element of (product J) holds

( x <= y iff for i being Element of I holds x . i <= y . i )

for J being RelStr-yielding non-Empty ManySortedSet of I

for x, y being Element of (product J) holds

( x <= y iff for i being Element of I holds x . i <= y . i )

proof end;

registration

let I be non empty set ;

let J be RelStr-yielding reflexive-yielding ManySortedSet of I;

let i be Element of I;

coherence

for b_{1} being RelStr st b_{1} = J . i holds

b_{1} is reflexive

end;
let J be RelStr-yielding reflexive-yielding ManySortedSet of I;

let i be Element of I;

coherence

for b

b

proof end;

registration

let I be non empty set ;

let J be RelStr-yielding non-Empty reflexive-yielding ManySortedSet of I;

coherence

product J is reflexive

end;
let J be RelStr-yielding non-Empty reflexive-yielding ManySortedSet of I;

coherence

product J is reflexive

proof end;

theorem Th29: :: WAYBEL_3:29

for I being non empty set

for J being RelStr-yielding non-Empty ManySortedSet of I st ( for i being Element of I holds J . i is transitive ) holds

product J is transitive

for J being RelStr-yielding non-Empty ManySortedSet of I st ( for i being Element of I holds J . i is transitive ) holds

product J is transitive

proof end;

theorem Th30: :: WAYBEL_3:30

for I being non empty set

for J being RelStr-yielding non-Empty ManySortedSet of I st ( for i being Element of I holds J . i is antisymmetric ) holds

product J is antisymmetric

for J being RelStr-yielding non-Empty ManySortedSet of I st ( for i being Element of I holds J . i is antisymmetric ) holds

product J is antisymmetric

proof end;

theorem Th31: :: WAYBEL_3:31

for I being non empty set

for J being RelStr-yielding non-Empty reflexive-yielding ManySortedSet of I st ( for i being Element of I holds J . i is complete LATTICE ) holds

product J is complete LATTICE

for J being RelStr-yielding non-Empty reflexive-yielding ManySortedSet of I st ( for i being Element of I holds J . i is complete LATTICE ) holds

product J is complete LATTICE

proof end;

theorem Th32: :: WAYBEL_3:32

for I being non empty set

for J being RelStr-yielding non-Empty reflexive-yielding ManySortedSet of I st ( for i being Element of I holds J . i is complete LATTICE ) holds

for X being Subset of (product J)

for i being Element of I holds (sup X) . i = sup (pi (X,i))

for J being RelStr-yielding non-Empty reflexive-yielding ManySortedSet of I st ( for i being Element of I holds J . i is complete LATTICE ) holds

for X being Subset of (product J)

for i being Element of I holds (sup X) . i = sup (pi (X,i))

proof end;

theorem :: WAYBEL_3:33

for I being non empty set

for J being RelStr-yielding non-Empty reflexive-yielding ManySortedSet of I st ( for i being Element of I holds J . i is complete LATTICE ) holds

for x, y being Element of (product J) holds

( x << y iff ( ( for i being Element of I holds x . i << y . i ) & ex K being finite Subset of I st

for i being Element of I st not i in K holds

x . i = Bottom (J . i) ) )

for J being RelStr-yielding non-Empty reflexive-yielding ManySortedSet of I st ( for i being Element of I holds J . i is complete LATTICE ) holds

for x, y being Element of (product J) holds

( x << y iff ( ( for i being Element of I holds x . i << y . i ) & ex K being finite Subset of I st

for i being Element of I st not i in K holds

x . i = Bottom (J . i) ) )

proof end;

theorem Th34: :: WAYBEL_3:34

for T being non empty TopSpace

for x, y being Element of (InclPoset the topology of T) st x is_way_below y holds

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

for x, y being Element of (InclPoset the topology of T) st x is_way_below y holds

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

proof end;

theorem Th35: :: WAYBEL_3:35

for T being non empty TopSpace

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

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

proof end;

theorem Th36: :: WAYBEL_3:36

for T being non empty TopSpace

for x being Element of (InclPoset the topology of T)

for X being Subset of T st x = X holds

( x is compact iff X is compact )

for x being Element of (InclPoset the topology of T)

for X being Subset of T st x = X holds

( x is compact iff X is compact )

proof end;

theorem :: WAYBEL_3:37

for T being non empty TopSpace

for x being Element of (InclPoset the topology of T) st x = the carrier of T holds

( x is compact iff T is compact )

for x being Element of (InclPoset the topology of T) st x = the carrier of T holds

( x is compact iff T is compact )

proof end;

:: deftheorem defines locally-compact WAYBEL_3:def 9 :

for T being non empty TopSpace holds

( T is locally-compact iff for x being Point of T

for X being Subset of T st x in X & X is open holds

ex Y being Subset of T st

( x in Int Y & Y c= X & Y is compact ) );

for T being non empty TopSpace holds

( T is locally-compact iff for x being Point of T

for X being Subset of T st x in X & X is open holds

ex Y being Subset of T st

( x in Int Y & Y c= X & Y is compact ) );

registration

for b_{1} being non empty TopSpace st b_{1} is compact & b_{1} is T_2 holds

( b_{1} is regular & b_{1} is normal & b_{1} is locally-compact )
end;

cluster non empty TopSpace-like T_2 compact -> non empty regular normal locally-compact for TopStruct ;

coherence for b

( b

proof end;

registration
end;

theorem Th38: :: WAYBEL_3:38

for T being non empty TopSpace

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

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

proof end;

theorem Th39: :: WAYBEL_3:39

for T being non empty TopSpace st T is locally-compact holds

for x, y being Element of (InclPoset the topology of T) st x << y holds

ex Z being Subset of T st

( x c= Z & Z c= y & Z is compact )

for x, y being Element of (InclPoset the topology of T) st x << y holds

ex Z being Subset of T st

( x c= Z & Z c= y & Z is compact )

proof end;

theorem :: WAYBEL_3:40

for T being non empty TopSpace st T is locally-compact & T is T_2 holds

for x, y being Element of (InclPoset the topology of T) st x << y holds

ex Z being Subset of T st

( Z = x & Cl Z c= y & Cl Z is compact )

for x, y being Element of (InclPoset the topology of T) st x << y holds

ex Z being Subset of T st

( Z = x & Cl Z c= y & Cl Z is compact )

proof end;

theorem :: WAYBEL_3:41

for X being non empty TopSpace st X is regular & InclPoset the topology of X is continuous holds

X is locally-compact

X is locally-compact

proof end;

theorem :: WAYBEL_3:42

for T being non empty TopSpace st T is locally-compact holds

InclPoset the topology of T is continuous

InclPoset the topology of T is continuous

proof end;