:: WAYBEL19 semantic presentation

K256() is Element of bool K252()

K252() is set

bool K252() is non empty set

K87() is set

bool K87() is non empty set

K181() is non empty strict TopSpace-like TopStruct

the carrier of K181() is non empty set

{} is empty finite V32() set

the empty finite V32() set is empty finite V32() set

1 is non empty set

{{},1} is non empty finite set

bool K256() is non empty set

{{}} is non empty finite V32() set

T is non empty RelStr

the carrier of T is non empty set

the InternalRel of T is Relation-like the carrier of T -defined the carrier of T -valued Element of bool [: the carrier of T, the carrier of T:]

[: the carrier of T, the carrier of T:] is non empty set

bool [: the carrier of T, the carrier of T:] is non empty set

RelStr(# the carrier of T, the InternalRel of T #) is strict RelStr

x is non empty RelStr

the carrier of x is non empty set

the InternalRel of x is Relation-like the carrier of x -defined the carrier of x -valued Element of bool [: the carrier of x, the carrier of x:]

[: the carrier of x, the carrier of x:] is non empty set

bool [: the carrier of x, the carrier of x:] is non empty set

RelStr(# the carrier of x, the InternalRel of x #) is strict RelStr

{ ((uparrow b

{ ((uparrow b

y9 is set

u is Element of the carrier of T

uparrow u is Element of bool the carrier of T

bool the carrier of T is non empty set

{u} is non empty finite Element of bool the carrier of T

uparrow {u} is Element of bool the carrier of T

(uparrow u) ` is Element of bool the carrier of T

the carrier of T \ (uparrow u) is set

W is Element of the carrier of x

uparrow W is Element of bool the carrier of x

bool the carrier of x is non empty set

{W} is non empty finite Element of bool the carrier of x

uparrow {W} is Element of bool the carrier of x

(uparrow W) ` is Element of bool the carrier of x

the carrier of x \ (uparrow W) is set

y9 is set

u is Element of the carrier of x

uparrow u is Element of bool the carrier of x

{u} is non empty finite Element of bool the carrier of x

uparrow {u} is Element of bool the carrier of x

(uparrow u) ` is Element of bool the carrier of x

the carrier of x \ (uparrow u) is set

W is Element of the carrier of T

uparrow W is Element of bool the carrier of T

{W} is non empty finite Element of bool the carrier of T

uparrow {W} is Element of bool the carrier of T

(uparrow W) ` is Element of bool the carrier of T

the carrier of T \ (uparrow W) is set

T is non empty trivial finite 1 -element TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() satisfying_axiom_of_approximation continuous connected up-complete /\-complete non void TopRelStr

the carrier of T is non empty trivial finite set

{ ((uparrow b

bool the carrier of T is non empty finite V32() set

bool (bool the carrier of T) is non empty finite V32() set

{ the carrier of T} is non empty finite V32() set

bool the carrier of T is non empty finite V32() Element of bool (bool the carrier of T)

x9 is set

y9 is Element of the carrier of T

uparrow y9 is non empty trivial finite directed filtered upper inaccessible_by_directed_joins Element of bool the carrier of T

{y9} is non empty trivial finite directed filtered upper inaccessible_by_directed_joins compact Element of bool the carrier of T

uparrow {y9} is non empty trivial finite directed filtered upper inaccessible_by_directed_joins Element of bool the carrier of T

(uparrow y9) ` is trivial finite directed filtered lower upper inaccessible_by_directed_joins closed_under_directed_sups property(S) Element of bool the carrier of T

the carrier of T \ (uparrow y9) is finite set

x9 is finite V32() Element of bool (bool the carrier of T)

the Element of the carrier of T is Element of the carrier of T

W is set

V is Element of the carrier of T

uparrow V is non empty trivial finite directed filtered upper inaccessible_by_directed_joins Element of bool the carrier of T

{V} is non empty trivial finite directed filtered upper inaccessible_by_directed_joins compact Element of bool the carrier of T

uparrow {V} is non empty trivial finite directed filtered upper inaccessible_by_directed_joins Element of bool the carrier of T

(uparrow V) ` is trivial finite directed filtered lower upper inaccessible_by_directed_joins closed_under_directed_sups property(S) Element of bool the carrier of T

the carrier of T \ (uparrow V) is finite set

uparrow the Element of the carrier of T is non empty trivial finite directed filtered upper inaccessible_by_directed_joins Element of bool the carrier of T

{ the Element of the carrier of T} is non empty trivial finite directed filtered upper inaccessible_by_directed_joins compact Element of bool the carrier of T

uparrow { the Element of the carrier of T} is non empty trivial finite directed filtered upper inaccessible_by_directed_joins Element of bool the carrier of T

(uparrow the Element of the carrier of T) ` is trivial finite directed filtered lower upper inaccessible_by_directed_joins closed_under_directed_sups property(S) Element of bool the carrier of T

the carrier of T \ (uparrow the Element of the carrier of T) is finite set

y9 is finite V32() Element of bool (bool the carrier of T)

FinMeetCl y9 is finite V32() Element of bool (bool the carrier of T)

{{}, the carrier of T} is non empty finite V32() set

y is non empty finite V32() V69(T) quasi_basis Element of bool (bool the carrier of T)

the topology of T is non empty finite V32() Element of bool (bool the carrier of T)

u is set

W is Element of the carrier of T

uparrow W is non empty trivial finite directed filtered upper inaccessible_by_directed_joins Element of bool the carrier of T

{W} is non empty trivial finite directed filtered upper inaccessible_by_directed_joins compact Element of bool the carrier of T

uparrow {W} is non empty trivial finite directed filtered upper inaccessible_by_directed_joins Element of bool the carrier of T

(uparrow W) ` is trivial finite directed filtered lower upper inaccessible_by_directed_joins closed_under_directed_sups property(S) Element of bool the carrier of T

the carrier of T \ (uparrow W) is finite set

V is set

(uparrow W) /\ u is trivial finite directed filtered upper inaccessible_by_directed_joins Element of bool the carrier of T

the non empty trivial finite 1 -element TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() satisfying_axiom_of_approximation continuous connected up-complete /\-complete strict non void () TopRelStr is non empty trivial finite 1 -element TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() satisfying_axiom_of_approximation continuous connected up-complete /\-complete strict non void () TopRelStr

T is non empty RelStr

the carrier of T is non empty set

{ ((uparrow b

bool the carrier of T is non empty Element of bool (bool the carrier of T)

bool the carrier of T is non empty set

bool (bool the carrier of T) is non empty set

y is set

x9 is Element of the carrier of T

uparrow x9 is Element of bool the carrier of T

{x9} is non empty finite Element of bool the carrier of T

uparrow {x9} is Element of bool the carrier of T

(uparrow x9) ` is Element of bool the carrier of T

the carrier of T \ (uparrow x9) is set

the InternalRel of T is Relation-like the carrier of T -defined the carrier of T -valued Element of bool [: the carrier of T, the carrier of T:]

[: the carrier of T, the carrier of T:] is non empty set

bool [: the carrier of T, the carrier of T:] is non empty set

y is Element of bool (bool the carrier of T)

FinMeetCl y is Element of bool (bool the carrier of T)

UniCl (FinMeetCl y) is Element of bool (bool the carrier of T)

TopRelStr(# the carrier of T, the InternalRel of T,(UniCl (FinMeetCl y)) #) is strict TopRelStr

TopStruct(# the carrier of T,(UniCl (FinMeetCl y)) #) is non empty strict TopStruct

the carrier of TopRelStr(# the carrier of T, the InternalRel of T,(UniCl (FinMeetCl y)) #) is set

the topology of TopRelStr(# the carrier of T, the InternalRel of T,(UniCl (FinMeetCl y)) #) is Element of bool (bool the carrier of TopRelStr(# the carrier of T, the InternalRel of T,(UniCl (FinMeetCl y)) #))

bool the carrier of TopRelStr(# the carrier of T, the InternalRel of T,(UniCl (FinMeetCl y)) #) is non empty set

bool (bool the carrier of TopRelStr(# the carrier of T, the InternalRel of T,(UniCl (FinMeetCl y)) #)) is non empty set

TopStruct(# the carrier of TopRelStr(# the carrier of T, the InternalRel of T,(UniCl (FinMeetCl y)) #), the topology of TopRelStr(# the carrier of T, the InternalRel of T,(UniCl (FinMeetCl y)) #) #) is strict TopStruct

y9 is non empty TopSpace-like TopStruct

the carrier of y9 is non empty set

bool the carrier of y9 is non empty set

bool (bool the carrier of y9) is non empty set

u is Element of bool (bool the carrier of TopRelStr(# the carrier of T, the InternalRel of T,(UniCl (FinMeetCl y)) #))

W is Element of bool (bool the carrier of y9)

union W is Element of bool the carrier of y9

the topology of y9 is non empty Element of bool (bool the carrier of y9)

union u is Element of bool the carrier of TopRelStr(# the carrier of T, the InternalRel of T,(UniCl (FinMeetCl y)) #)

u is Element of bool the carrier of TopRelStr(# the carrier of T, the InternalRel of T,(UniCl (FinMeetCl y)) #)

W is Element of bool the carrier of TopRelStr(# the carrier of T, the InternalRel of T,(UniCl (FinMeetCl y)) #)

u /\ W is Element of bool the carrier of TopRelStr(# the carrier of T, the InternalRel of T,(UniCl (FinMeetCl y)) #)

u is non empty TopSpace-like strict TopRelStr

the carrier of u is non empty set

{ ((uparrow b

the InternalRel of u is Relation-like the carrier of u -defined the carrier of u -valued Element of bool [: the carrier of u, the carrier of u:]

[: the carrier of u, the carrier of u:] is non empty set

bool [: the carrier of u, the carrier of u:] is non empty set

RelStr(# the carrier of u, the InternalRel of u #) is strict RelStr

RelStr(# the carrier of T, the InternalRel of T #) is strict RelStr

the carrier of y9 is non empty set

bool the carrier of y9 is non empty set

bool (bool the carrier of y9) is non empty set

V is non empty V69(y9) quasi_basis Element of bool (bool the carrier of y9)

the topology of u is non empty Element of bool (bool the carrier of u)

bool the carrier of u is non empty set

bool (bool the carrier of u) is non empty set

UniCl V is Element of bool (bool the carrier of y9)

the topology of y9 is non empty Element of bool (bool the carrier of y9)

T is non empty RelStr

T is non empty TopSpace-like () TopRelStr

the carrier of T is non empty set

the InternalRel of T is Relation-like the carrier of T -defined the carrier of T -valued Element of bool [: the carrier of T, the carrier of T:]

[: the carrier of T, the carrier of T:] is non empty set

bool [: the carrier of T, the carrier of T:] is non empty set

RelStr(# the carrier of T, the InternalRel of T #) is strict RelStr

x is non empty TopSpace-like () TopRelStr

the carrier of x is non empty set

the InternalRel of x is Relation-like the carrier of x -defined the carrier of x -valued Element of bool [: the carrier of x, the carrier of x:]

[: the carrier of x, the carrier of x:] is non empty set

bool [: the carrier of x, the carrier of x:] is non empty set

RelStr(# the carrier of x, the InternalRel of x #) is strict RelStr

the topology of T is non empty Element of bool (bool the carrier of T)

bool the carrier of T is non empty set

bool (bool the carrier of T) is non empty set

the topology of x is non empty Element of bool (bool the carrier of x)

bool the carrier of x is non empty set

bool (bool the carrier of x) is non empty set

{ ((uparrow b

{ ((uparrow b

T is non empty RelStr

the carrier of T is non empty set

bool the carrier of T is non empty set

bool (bool the carrier of T) is non empty set

the non empty TopSpace-like () TopAugmentation of T is non empty TopSpace-like () TopAugmentation of T

y is Element of bool (bool the carrier of T)

x9 is Element of bool (bool the carrier of T)

the topology of the non empty TopSpace-like () TopAugmentation of T is non empty Element of bool (bool the carrier of the non empty TopSpace-like () TopAugmentation of T)

the carrier of the non empty TopSpace-like () TopAugmentation of T is non empty set

bool the carrier of the non empty TopSpace-like () TopAugmentation of T is non empty set

bool (bool the carrier of the non empty TopSpace-like () TopAugmentation of T) is non empty set

the non empty TopSpace-like () TopAugmentation of T is non empty TopSpace-like () TopAugmentation of T

the carrier of the non empty TopSpace-like () TopAugmentation of T is non empty set

the InternalRel of the non empty TopSpace-like () TopAugmentation of T is Relation-like the carrier of the non empty TopSpace-like () TopAugmentation of T -defined the carrier of the non empty TopSpace-like () TopAugmentation of T -valued Element of bool [: the carrier of the non empty TopSpace-like () TopAugmentation of T, the carrier of the non empty TopSpace-like () TopAugmentation of T:]

[: the carrier of the non empty TopSpace-like () TopAugmentation of T, the carrier of the non empty TopSpace-like () TopAugmentation of T:] is non empty set

bool [: the carrier of the non empty TopSpace-like () TopAugmentation of T, the carrier of the non empty TopSpace-like () TopAugmentation of T:] is non empty set

RelStr(# the carrier of the non empty TopSpace-like () TopAugmentation of T, the InternalRel of the non empty TopSpace-like () TopAugmentation of T #) is strict RelStr

the InternalRel of T is Relation-like the carrier of T -defined the carrier of T -valued Element of bool [: the carrier of T, the carrier of T:]

[: the carrier of T, the carrier of T:] is non empty set

bool [: the carrier of T, the carrier of T:] is non empty set

RelStr(# the carrier of T, the InternalRel of T #) is strict RelStr

the topology of the non empty TopSpace-like () TopAugmentation of T is non empty Element of bool (bool the carrier of the non empty TopSpace-like () TopAugmentation of T)

bool the carrier of the non empty TopSpace-like () TopAugmentation of T is non empty set

bool (bool the carrier of the non empty TopSpace-like () TopAugmentation of T) is non empty set

y is Element of bool (bool the carrier of T)

x9 is non empty TopSpace-like () TopAugmentation of T

the topology of x9 is non empty Element of bool (bool the carrier of x9)

the carrier of x9 is non empty set

bool the carrier of x9 is non empty set

bool (bool the carrier of x9) is non empty set

the InternalRel of x9 is Relation-like the carrier of x9 -defined the carrier of x9 -valued Element of bool [: the carrier of x9, the carrier of x9:]

[: the carrier of x9, the carrier of x9:] is non empty set

bool [: the carrier of x9, the carrier of x9:] is non empty set

RelStr(# the carrier of x9, the InternalRel of x9 #) is strict RelStr

T is non empty RelStr

the carrier of T is non empty set

the InternalRel of T is Relation-like the carrier of T -defined the carrier of T -valued Element of bool [: the carrier of T, the carrier of T:]

[: the carrier of T, the carrier of T:] is non empty set

bool [: the carrier of T, the carrier of T:] is non empty set

RelStr(# the carrier of T, the InternalRel of T #) is strict RelStr

x is non empty RelStr

the carrier of x is non empty set

the InternalRel of x is Relation-like the carrier of x -defined the carrier of x -valued Element of bool [: the carrier of x, the carrier of x:]

[: the carrier of x, the carrier of x:] is non empty set

bool [: the carrier of x, the carrier of x:] is non empty set

RelStr(# the carrier of x, the InternalRel of x #) is strict RelStr

(T) is Element of bool (bool the carrier of T)

bool the carrier of T is non empty set

bool (bool the carrier of T) is non empty set

(x) is Element of bool (bool the carrier of x)

bool the carrier of x is non empty set

bool (bool the carrier of x) is non empty set

the non empty TopSpace-like () TopAugmentation of T is non empty TopSpace-like () TopAugmentation of T

the carrier of the non empty TopSpace-like () TopAugmentation of T is non empty set

the InternalRel of the non empty TopSpace-like () TopAugmentation of T is Relation-like the carrier of the non empty TopSpace-like () TopAugmentation of T -defined the carrier of the non empty TopSpace-like () TopAugmentation of T -valued Element of bool [: the carrier of the non empty TopSpace-like () TopAugmentation of T, the carrier of the non empty TopSpace-like () TopAugmentation of T:]

[: the carrier of the non empty TopSpace-like () TopAugmentation of T, the carrier of the non empty TopSpace-like () TopAugmentation of T:] is non empty set

bool [: the carrier of the non empty TopSpace-like () TopAugmentation of T, the carrier of the non empty TopSpace-like () TopAugmentation of T:] is non empty set

RelStr(# the carrier of the non empty TopSpace-like () TopAugmentation of T, the InternalRel of the non empty TopSpace-like () TopAugmentation of T #) is strict RelStr

the topology of the non empty TopSpace-like () TopAugmentation of T is non empty Element of bool (bool the carrier of the non empty TopSpace-like () TopAugmentation of T)

bool the carrier of the non empty TopSpace-like () TopAugmentation of T is non empty set

bool (bool the carrier of the non empty TopSpace-like () TopAugmentation of T) is non empty set

T is non empty () TopRelStr

the carrier of T is non empty set

{ ((uparrow b

y is Element of the carrier of T

uparrow y is Element of bool the carrier of T

bool the carrier of T is non empty set

{y} is non empty finite Element of bool the carrier of T

uparrow {y} is Element of bool the carrier of T

(uparrow y) ` is Element of bool the carrier of T

the carrier of T \ (uparrow y) is set

bool (bool the carrier of T) is non empty set

the topology of T is Element of bool (bool the carrier of T)

x9 is Element of the carrier of T

uparrow x9 is Element of bool the carrier of T

{x9} is non empty finite Element of bool the carrier of T

uparrow {x9} is Element of bool the carrier of T

(uparrow x9) ` is Element of bool the carrier of T

the carrier of T \ (uparrow x9) is set

[#] T is non empty non proper dense lower upper Element of bool the carrier of T

([#] T) \ (uparrow y) is Element of bool the carrier of T

T is non empty transitive () TopRelStr

the carrier of T is non empty set

bool the carrier of T is non empty set

bool (bool the carrier of T) is non empty set

{ ((uparrow b

y is Element of bool the carrier of T

the topology of T is Element of bool (bool the carrier of T)

x9 is Element of the carrier of T

y9 is Element of the carrier of T

x is V69(T) quasi_prebasis Element of bool (bool the carrier of T)

FinMeetCl x is Element of bool (bool the carrier of T)

u is V69(T) quasi_basis Element of bool (bool the carrier of T)

UniCl u is Element of bool (bool the carrier of T)

W is Element of bool (bool the carrier of T)

union W is Element of bool the carrier of T

V is set

x is Element of bool (bool the carrier of T)

Intersect x is Element of bool the carrier of T

z is set

Y is Element of the carrier of T

uparrow Y is upper Element of bool the carrier of T

{Y} is non empty finite Element of bool the carrier of T

uparrow {Y} is upper Element of bool the carrier of T

(uparrow Y) ` is lower Element of bool the carrier of T

the carrier of T \ (uparrow Y) is set

(uparrow Y) /\ z is Element of bool the carrier of T

{} T is empty proper finite V32() boundary directed filtered lower upper Element of bool the carrier of T

T is non empty transitive () TopRelStr

the carrier of T is non empty set

bool the carrier of T is non empty set

x is Element of bool the carrier of T

[#] T is non empty non proper dense lower upper Element of bool the carrier of T

([#] T) \ x is Element of bool the carrier of T

the topology of T is Element of bool (bool the carrier of T)

bool (bool the carrier of T) is non empty set

x ` is Element of bool the carrier of T

the carrier of T \ x is set

y is Element of the carrier of T

x9 is Element of the carrier of T

T is non empty TopSpace-like TopRelStr

the carrier of T is non empty set

bool the carrier of T is non empty set

{ ((uparrow b

bool (bool the carrier of T) is non empty set

{ ((uparrow b

bool the carrier of T is non empty Element of bool (bool the carrier of T)

y is set

x9 is Element of the carrier of T

uparrow x9 is Element of bool the carrier of T

{x9} is non empty finite compact Element of bool the carrier of T

uparrow {x9} is Element of bool the carrier of T

(uparrow x9) ` is Element of bool the carrier of T

the carrier of T \ (uparrow x9) is set

y is Element of bool (bool the carrier of T)

u is Element of bool (bool the carrier of T)

FinMeetCl u is Element of bool (bool the carrier of T)

x9 is non empty RelStr

the carrier of x9 is non empty set

bool the carrier of x9 is non empty set

W is set

V is Element of bool the carrier of T

uparrow V is Element of bool the carrier of T

(uparrow V) ` is Element of bool the carrier of T

the carrier of T \ (uparrow V) is set

{ (uparrow b

z is set

Y is Element of the carrier of T

uparrow Y is Element of bool the carrier of T

{Y} is non empty finite compact Element of bool the carrier of T

uparrow {Y} is Element of bool the carrier of T

z is Element of bool (bool the carrier of T)

Y is Element of bool (bool the carrier of T)

union Y is Element of bool the carrier of T

COMPLEMENT Y is Element of bool (bool the carrier of T)

Intersect (COMPLEMENT Y) is Element of bool the carrier of T

bool (bool the carrier of x9) is non empty set

I2 is Element of bool (bool the carrier of x9)

{ H

COMPLEMENT I2 is Element of bool (bool the carrier of x9)

{ (H

Y is set

Z is Element of the carrier of T

uparrow Z is Element of bool the carrier of T

{Z} is non empty finite compact Element of bool the carrier of T

uparrow {Z} is Element of bool the carrier of T

(uparrow Z) ` is Element of bool the carrier of T

the carrier of T \ (uparrow Z) is set

{ H

W is set

V is Element of bool (bool the carrier of T)

Intersect V is Element of bool the carrier of T

x is set

z is Element of the carrier of T

uparrow z is Element of bool the carrier of T

{z} is non empty finite compact Element of bool the carrier of T

uparrow {z} is Element of bool the carrier of T

(uparrow z) ` is Element of bool the carrier of T

the carrier of T \ (uparrow z) is set

x is Relation-like Function-like set

dom x is set

rng x is set

z is Element of bool the carrier of T

{ (uparrow b

I2 is set

Y is Element of the carrier of T

uparrow Y is Element of bool the carrier of T

{Y} is non empty finite compact Element of bool the carrier of T

uparrow {Y} is Element of bool the carrier of T

I2 is Element of bool (bool the carrier of T)

Y is Element of bool (bool the carrier of T)

Z is Element of bool (bool the carrier of x9)

{ H

COMPLEMENT Z is Element of bool (bool the carrier of x9)

{ (H

COMPLEMENT Y is Element of bool (bool the carrier of T)

J2 is set

y is Element of the carrier of x9

uparrow y is Element of bool the carrier of x9

{y} is non empty finite Element of bool the carrier of x9

uparrow {y} is Element of bool the carrier of x9

(uparrow y) ` is Element of bool the carrier of x9

the carrier of x9 \ (uparrow y) is set

a is set

x . a is set

AA is Element of the carrier of T

uparrow AA is Element of bool the carrier of T

{AA} is non empty finite compact Element of bool the carrier of T

uparrow {AA} is Element of bool the carrier of T

(uparrow AA) ` is Element of bool the carrier of T

the carrier of T \ (uparrow AA) is set

J2 is set

x . J2 is set

y is Element of the carrier of T

uparrow y is Element of bool the carrier of T

{y} is non empty finite compact Element of bool the carrier of T

uparrow {y} is Element of bool the carrier of T

(uparrow y) ` is Element of bool the carrier of T

the carrier of T \ (uparrow y) is set

uparrow z is Element of bool the carrier of T

union Y is Element of bool the carrier of T

(uparrow z) ` is Element of bool the carrier of T

the carrier of T \ (uparrow z) is set

T is non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete non void () TopRelStr

the carrier of T is non empty set

x is non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete non void () TopRelStr

the carrier of x is non empty set

[: the carrier of T, the carrier of x:] is non empty set

bool [: the carrier of T, the carrier of x:] is non empty set

bool the carrier of T is non empty set

bool the carrier of x is non empty set

bool (bool the carrier of x) is non empty set

{ ((uparrow b

x9 is Relation-like the carrier of T -defined the carrier of x -valued Function-like V18( the carrier of T, the carrier of x) Element of bool [: the carrier of T, the carrier of x:]

y9 is Element of bool the carrier of x

y9 ` is Element of bool the carrier of x

the carrier of x \ y9 is set

x9 " (y9 `) is Element of bool the carrier of T

x9 .: (x9 " (y9 `)) is Element of bool the carrier of x

y is V69(x) quasi_prebasis Element of bool (bool the carrier of x)

u is Element of the carrier of x

uparrow u is non empty filtered upper Element of bool the carrier of x

{u} is non empty finite compact Element of bool the carrier of x

uparrow {u} is non empty upper Element of bool the carrier of x

(uparrow u) ` is lower property(S) Element of bool the carrier of x

the carrier of x \ (uparrow u) is set

x9 " (uparrow u) is Element of bool the carrier of T

"/\" ((x9 " (uparrow u)),T) is Element of the carrier of T

{} T is empty proper finite V32() open closed boundary nowhere_dense directed filtered lower upper closed_under_directed_sups property(S) Element of bool the carrier of T

x9 . ("/\" ((x9 " (uparrow u)),T)) is Element of the carrier of x

"/\" ((x9 .: (x9 " (y9 `))),x) is Element of the carrier of x

"/\" ((y9 `),x) is Element of the carrier of x

uparrow ("/\" ((x9 " (uparrow u)),T)) is non empty filtered upper Element of bool the carrier of T

{("/\" ((x9 " (uparrow u)),T))} is non empty finite compact Element of bool the carrier of T

uparrow {("/\" ((x9 " (uparrow u)),T))} is non empty upper Element of bool the carrier of T

V is set

x is Element of the carrier of T

V is set

x is Element of the carrier of T

{("/\" ((x9 " (uparrow u)),T)),x} is non empty finite Element of bool the carrier of T

("/\" ((x9 " (uparrow u)),T)) "/\" x is Element of the carrier of T

x9 . (("/\" ((x9 " (uparrow u)),T)) "/\" x) is Element of the carrier of x

x9 . x is Element of the carrier of x

(x9 . ("/\" ((x9 " (uparrow u)),T))) "/\" (x9 . x) is Element of the carrier of x

{} T is empty proper finite V32() open closed boundary nowhere_dense directed filtered lower upper closed_under_directed_sups property(S) Element of bool the carrier of T

T is non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete non void () TopRelStr

the carrier of T is non empty set

x is non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete non void () TopRelStr

the carrier of x is non empty set

[: the carrier of T, the carrier of x:] is non empty set

bool [: the carrier of T, the carrier of x:] is non empty set

y is Relation-like the carrier of T -defined the carrier of x -valued Function-like V18( the carrier of T, the carrier of x) Element of bool [: the carrier of T, the carrier of x:]

bool the carrier of T is non empty set

x9 is non empty Element of bool the carrier of T

T is non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete non void () TopRelStr

the carrier of T is non empty set

bool the carrier of T is non empty set

bool (bool the carrier of T) is non empty set

x is V69(T) quasi_prebasis Element of bool (bool the carrier of T)

y is non empty filtered Element of bool the carrier of T

"/\" (y,T) is Element of the carrier of T

Cl y is closed Element of bool the carrier of T

y opp+id is non empty reflexive transitive strict directed non void NetStr over T

subrelstr y is strict reflexive transitive antisymmetric full SubRelStr of T

K448(T,(subrelstr y)) is Relation-like the carrier of (subrelstr y) -defined the carrier of T -valued Function-like V18( the carrier of (subrelstr y), the carrier of T) Element of bool [: the carrier of (subrelstr y), the carrier of T:]

the carrier of (subrelstr y) is set

[: the carrier of (subrelstr y), the carrier of T:] is set

bool [: the carrier of (subrelstr y), the carrier of T:] is non empty set

(subrelstr y) opp+id is strict strict directed NetStr over subrelstr y

K448(T,(subrelstr y)) * ((subrelstr y) opp+id) is strict NetStr over T

u is Element of bool the carrier of T

W is set

the carrier of (y opp+id) is non empty set

V is Element of the carrier of (y opp+id)

x is Element of the carrier of (y opp+id)

(y opp+id) . x is Element of the carrier of T

the mapping of (y opp+id) is non empty Relation-like the carrier of (y opp+id) -defined the carrier of T -valued Function-like V18( the carrier of (y opp+id), the carrier of T) Element of bool [: the carrier of (y opp+id), the carrier of T:]

[: the carrier of (y opp+id), the carrier of T:] is non empty set

bool [: the carrier of (y opp+id), the carrier of T:] is non empty set

K76( the carrier of (y opp+id), the carrier of T, the mapping of (y opp+id),x) is Element of the carrier of T

T ~ is non empty strict reflexive transitive antisymmetric non void RelStr

the InternalRel of T is non empty Relation-like the carrier of T -defined the carrier of T -valued Element of bool [: the carrier of T, the carrier of T:]

[: the carrier of T, the carrier of T:] is non empty set

bool [: the carrier of T, the carrier of T:] is non empty set

the InternalRel of T ~ is Relation-like the carrier of T -defined the carrier of T -valued Element of bool [: the carrier of T, the carrier of T:]

RelStr(# the carrier of T,( the InternalRel of T ~) #) is strict RelStr

the carrier of (T ~) is non empty set

z is Element of the carrier of (T ~)

Y is Element of the carrier of (T ~)

~ Y is Element of the carrier of T

~ z is Element of the carrier of T

the carrier of (y opp+id) is non empty set

netmap ((y opp+id),T) is Relation-like the carrier of (y opp+id) -defined the carrier of T -valued Function-like V18( the carrier of (y opp+id), the carrier of T) Element of bool [: the carrier of (y opp+id), the carrier of T:]

[: the carrier of (y opp+id), the carrier of T:] is non empty set

bool [: the carrier of (y opp+id), the carrier of T:] is non empty set

the mapping of (y opp+id) is non empty Relation-like the carrier of (y opp+id) -defined the carrier of T -valued Function-like V18( the carrier of (y opp+id), the carrier of T) Element of bool [: the carrier of (y opp+id), the carrier of T:]

rng (netmap ((y opp+id),T)) is Element of bool the carrier of T

u is set

dom (netmap ((y opp+id),T)) is Element of bool the carrier of (y opp+id)

bool the carrier of (y opp+id) is non empty set

W is set

(netmap ((y opp+id),T)) . W is set

V is Element of the carrier of (y opp+id)

(y opp+id) . V is Element of the carrier of T

K76( the carrier of (y opp+id), the carrier of T, the mapping of (y opp+id),V) is Element of the carrier of T

T is non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete non void () TopRelStr

the carrier of T is non empty set

x is non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete non void () TopRelStr

the carrier of x is non empty set

[: the carrier of T, the carrier of x:] is non empty set

bool [: the carrier of T, the carrier of x:] is non empty set

bool the carrier of T is non empty set

bool (bool the carrier of T) is non empty set

{ ((uparrow b

x9 is Relation-like the carrier of T -defined the carrier of x -valued Function-like V18( the carrier of T, the carrier of x) Element of bool [: the carrier of T, the carrier of x:]

y9 is Element of bool the carrier of T

x9 .: y9 is Element of bool the carrier of x

bool the carrier of x is non empty set

"/\" ((x9 .: y9),x) is Element of the carrier of x

"/\" (y9,T) is Element of the carrier of T

K76( the carrier of T, the carrier of x,x9,("/\" (y9,T))) is Element of the carrier of x

y is V69(T) quasi_prebasis Element of bool (bool the carrier of T)

u is Element of bool the carrier of T

W is Element of the carrier of T

uparrow W is non empty filtered upper Element of bool the carrier of T

{W} is non empty finite compact Element of bool the carrier of T

uparrow {W} is non empty upper Element of bool the carrier of T

(uparrow W) ` is lower property(S) Element of bool the carrier of T

the carrier of T \ (uparrow W) is set

V is Element of the carrier of T

Cl y9 is closed Element of bool the carrier of T

u is Element of the carrier of T

W is Element of the carrier of T

K76( the carrier of T, the carrier of x,x9,u) is Element of the carrier of x

K76( the carrier of T, the carrier of x,x9,W) is Element of the carrier of x

x9 . u is Element of the carrier of x

uparrow (x9 . u) is non empty filtered upper Element of bool the carrier of x

{(x9 . u)} is non empty finite compact Element of bool the carrier of x

uparrow {(x9 . u)} is non empty upper Element of bool the carrier of x

x9 " (uparrow (x9 . u)) is Element of bool the carrier of T

x9 . W is Element of the carrier of x

x9 . ("/\" (y9,T)) is Element of the carrier of x

u is Element of the carrier of x

W is set

x9 . W is set

V is Element of the carrier of T

uparrow ("/\" ((x9 .: y9),x)) is non empty filtered upper Element of bool the carrier of x

{("/\" ((x9 .: y9),x))} is non empty finite compact Element of bool the carrier of x

uparrow {("/\" ((x9 .: y9),x))} is non empty upper Element of bool the carrier of x

x9 " (uparrow ("/\" ((x9 .: y9),x))) is Element of bool the carrier of T

u is set

W is Element of the carrier of T

x9 . W is Element of the carrier of x

Cl (x9 " (uparrow ("/\" ((x9 .: y9),x)))) is closed Element of bool the carrier of T

T is non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete non void () TopRelStr

the carrier of T is non empty set

x is non empty TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete non void () TopRelStr

the carrier of x is non empty set

[: the carrier of T, the carrier of x:] is non empty set

bool [: the carrier of T, the carrier of x:] is non empty set

bool the carrier of T is non empty set

y is Relation-like the carrier of T -defined the carrier of x -valued Function-like V18( the carrier of T, the carrier of x) Element of bool [: the carrier of T, the carrier of x:]

x9 is non empty filtered Element of bool the carrier of T

T is non empty TopSpace-like reflexive transitive non void () TopRelStr

the carrier of T is non empty set

x is Element of the carrier of T

{x} is non empty finite compact Element of bool the carrier of T

bool the carrier of T is non empty set

Cl {x} is closed Element of bool the carrier of T

uparrow x is non empty filtered upper Element of bool the carrier of T

uparrow {x} is non empty upper Element of bool the carrier of T

y is Element of the carrier of T

uparrow (Cl {x}) is upper Element of bool the carrier of T

T is non empty TopSpace-like reflexive transitive antisymmetric non void TopRelStr

the carrier of T is non empty set

x is Element of the carrier of T

y is Element of the carrier of T

x9 is Element of the carrier of T

uparrow x9 is non empty filtered upper Element of bool the carrier of T

bool the carrier of T is non empty set

{x9} is non empty finite compact Element of bool the carrier of T

uparrow {x9} is non empty upper Element of bool the carrier of T

(uparrow x9) ` is lower Element of bool the carrier of T

the carrier of T \ (uparrow x9) is set

y9 is Element of the carrier of T

uparrow y9 is non empty filtered upper Element of bool the carrier of T

{y9} is non empty finite compact Element of bool the carrier of T

uparrow {y9} is non empty upper Element of bool the carrier of T

(uparrow y9) ` is lower Element of bool the carrier of T

the carrier of T \ (uparrow y9) is set

T is non empty lower-bounded RelStr

x is non empty TopAugmentation of T

the carrier of T is non empty set

the InternalRel of T is Relation-like the carrier of T -defined the carrier of T -valued Element of bool [: the carrier of T, the carrier of T:]

[: the carrier of T, the carrier of T:] is non empty set

bool [: the carrier of T, the carrier of T:] is non empty set

RelStr(# the carrier of T, the InternalRel of T #) is strict RelStr

the carrier of x is non empty set

the InternalRel of x is Relation-like the carrier of x -defined the carrier of x -valued Element of bool [: the carrier of x, the carrier of x:]

[: the carrier of x, the carrier of x:] is non empty set

bool [: the carrier of x, the carrier of x:] is non empty set

RelStr(# the carrier of x, the InternalRel of x #) is strict RelStr

T is non empty RelStr

the carrier of T is non empty set

x is non empty RelStr

the carrier of x is non empty set

[:T,x:] is non empty strict RelStr

the carrier of [:T,x:] is non empty set

y is Element of the carrier of T

uparrow y is Element of bool the carrier of T

bool the carrier of T is non empty set

{y} is non empty finite Element of bool the carrier of T

uparrow {y} is Element of bool the carrier of T

(uparrow y) ` is Element of bool the carrier of T

the carrier of T \ (uparrow y) is set

[:((uparrow y) `), the carrier of x:] is set

x9 is Element of the carrier of x

[y,x9] is Element of the carrier of [:T,x:]

{y,x9} is non empty finite set

{y} is non empty finite set

{{y,x9},{y}} is non empty finite V32() set

uparrow [y,x9] is Element of bool the carrier of [:T,x:]

bool the carrier of [:T,x:] is non empty set

{[y,x9]} is non empty finite Element of bool the carrier of [:T,x:]

uparrow {[y,x9]} is Element of bool the carrier of [:T,x:]

(uparrow [y,x9]) ` is Element of bool the carrier of [:T,x:]

the carrier of [:T,x:] \ (uparrow [y,x9]) is set

uparrow x9 is Element of bool the carrier of x

bool the carrier of x is non empty set

{x9} is non empty finite Element of bool the carrier of x

uparrow {x9} is Element of bool the carrier of x

(uparrow x9) ` is Element of bool the carrier of x

the carrier of x \ (uparrow x9) is set

[: the carrier of T,((uparrow x9) `):] is set

[:((uparrow y) `), the carrier of x:] \/ [: the carrier of T,((uparrow x9) `):] is set

[: the carrier of T, the carrier of x:] is non empty set

[: the carrier of T, the carrier of x:] \ (uparrow [y,x9]) is Relation-like the carrier of T -defined the carrier of x -valued Element of bool [: the carrier of T, the carrier of x:]

bool [: the carrier of T, the carrier of x:] is non empty set

[:(uparrow y),(uparrow x9):] is Element of bool the carrier of [:T,x:]

[: the carrier of T, the carrier of x:] \ [:(uparrow y),(uparrow x9):] is Relation-like the carrier of T -defined the carrier of x -valued Element of bool [: the carrier of T, the carrier of x:]

T is non empty reflexive transitive antisymmetric lower-bounded non void RelStr

x is non empty reflexive transitive antisymmetric lower-bounded non void RelStr

[:T,x:] is non empty strict reflexive transitive antisymmetric non void RelStr

([:T,x:]) is Element of bool (bool the carrier of [:T,x:])

the carrier of [:T,x:] is non empty set

bool the carrier of [:T,x:] is non empty set

bool (bool the carrier of [:T,x:]) is non empty set

the non empty TopSpace-like T_0 reflexive transitive antisymmetric non void () TopAugmentation of [:T,x:] is non empty TopSpace-like T_0 reflexive transitive antisymmetric non void () TopAugmentation of [:T,x:]

the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric non void () TopAugmentation of [:T,x:] is non empty set

bool the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric non void () TopAugmentation of [:T,x:] is non empty set

bool (bool the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric non void () TopAugmentation of [:T,x:]) is non empty set

{ ((uparrow b

y9 is non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded non void () TopAugmentation of T

the carrier of y9 is non empty set

bool the carrier of y9 is non empty set

bool (bool the carrier of y9) is non empty set

{ ((uparrow b

W is non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded non void () TopAugmentation of x

[:y9,W:] is non empty strict TopSpace-like TopStruct

the topology of [:y9,W:] is non empty Element of bool (bool the carrier of [:y9,W:])

the carrier of [:y9,W:] is non empty set

bool the carrier of [:y9,W:] is non empty set

bool (bool the carrier of [:y9,W:]) is non empty set

the carrier of W is non empty set

u is V69(y9) quasi_prebasis Element of bool (bool the carrier of y9)

{ [:b

the InternalRel of W is non empty Relation-like the carrier of W -defined the carrier of W -valued Element of bool [: the carrier of W, the carrier of W:]

[: the carrier of W, the carrier of W:] is non empty set

bool [: the carrier of W, the carrier of W:] is non empty set

RelStr(# the carrier of W, the InternalRel of W #) is strict RelStr

the carrier of x is non empty set

the InternalRel of x is non empty Relation-like the carrier of x -defined the carrier of x -valued Element of bool [: the carrier of x, the carrier of x:]

[: the carrier of x, the carrier of x:] is non empty set

bool [: the carrier of x, the carrier of x:] is non empty set

RelStr(# the carrier of x, the InternalRel of x #) is strict RelStr

bool the carrier of W is non empty set

bool (bool the carrier of W) is non empty set

{ ((uparrow b

the InternalRel of y9 is non empty Relation-like the carrier of y9 -defined the carrier of y9 -valued Element of bool [: the carrier of y9, the carrier of y9:]

[: the carrier of y9, the carrier of y9:] is non empty set

bool [: the carrier of y9, the carrier of y9:] is non empty set

RelStr(# the carrier of y9, the InternalRel of y9 #) is strict RelStr

the carrier of T is non empty set

the InternalRel of T is non empty Relation-like the carrier of T -defined the carrier of T -valued Element of bool [: the carrier of T, the carrier of T:]

[: the carrier of T, the carrier of T:] is non empty set

bool [: the carrier of T, the carrier of T:] is non empty set

RelStr(# the carrier of T, the InternalRel of T #) is strict RelStr

[: the carrier of T, the carrier of x:] is non empty set

the InternalRel of the non empty TopSpace-like T_0 reflexive transitive antisymmetric non void () TopAugmentation of [:T,x:] is non empty Relation-like the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric non void () TopAugmentation of [:T,x:] -defined the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric non void () TopAugmentation of [:T,x:] -valued Element of bool [: the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric non void () TopAugmentation of [:T,x:], the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric non void () TopAugmentation of [:T,x:]:]

[: the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric non void () TopAugmentation of [:T,x:], the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric non void () TopAugmentation of [:T,x:]:] is non empty set

bool [: the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric non void () TopAugmentation of [:T,x:], the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric non void () TopAugmentation of [:T,x:]:] is non empty set

RelStr(# the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric non void () TopAugmentation of [:T,x:], the InternalRel of the non empty TopSpace-like T_0 reflexive transitive antisymmetric non void () TopAugmentation of [:T,x:] #) is strict RelStr

x9 is V69( the non empty TopSpace-like T_0 reflexive transitive antisymmetric non void () TopAugmentation of [:T,x:]) quasi_prebasis Element of bool (bool the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric non void () TopAugmentation of [:T,x:])

Y is set

[#] W is non empty non proper open closed dense non boundary filtered lower upper inaccessible_by_directed_joins closed_under_directed_sups Element of bool the carrier of W

I2 is Element of the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric non void () TopAugmentation of [:T,x:]

uparrow I2 is non empty filtered upper Element of bool the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric non void () TopAugmentation of [:T,x:]

{I2} is non empty finite compact Element of bool the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric non void () TopAugmentation of [:T,x:]

uparrow {I2} is non empty upper Element of bool the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric non void () TopAugmentation of [:T,x:]

(uparrow I2) ` is lower Element of bool the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric non void () TopAugmentation of [:T,x:]

the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric non void () TopAugmentation of [:T,x:] \ (uparrow I2) is set

Y is set

Z is set

[Y,Z] is set

{Y,Z} is non empty finite set

{Y} is non empty finite set

{{Y,Z},{Y}} is non empty finite V32() set

y is Element of the carrier of T

J2 is Element of the carrier of x

[y,J2] is Element of the carrier of [:T,x:]

{y,J2} is non empty finite set

{y} is non empty finite set

{{y,J2},{y}} is non empty finite V32() set

uparrow [y,J2] is non empty filtered upper Element of bool the carrier of [:T,x:]

{[y,J2]} is non empty finite Element of bool the carrier of [:T,x:]

uparrow {[y,J2]} is non empty upper Element of bool the carrier of [:T,x:]

uparrow y is non empty filtered upper Element of bool the carrier of T

bool the carrier of T is non empty set

{y} is non empty finite Element of bool the carrier of T

uparrow {y} is non empty upper Element of bool the carrier of T

(uparrow y) ` is lower Element of bool the carrier of T

the carrier of T \ (uparrow y) is set

[#] x is non empty non proper filtered lower upper inaccessible_by_directed_joins closed_under_directed_sups Element of bool the carrier of x

bool the carrier of x is non empty set

[:((uparrow y) `),([#] x):] is lower Element of bool the carrier of [:T,x:]

[#] T is non empty non proper filtered lower upper inaccessible_by_directed_joins closed_under_directed_sups Element of bool the carrier of T

uparrow J2 is non empty filtered upper Element of bool the carrier of x

{J2} is non empty finite Element of bool the carrier of x

uparrow {J2} is non empty upper Element of bool the carrier of x

(uparrow J2) ` is lower Element of bool the carrier of x

the carrier of x \ (uparrow J2) is set

[:([#] T),((uparrow J2) `):] is lower Element of bool the carrier of [:T,x:]

[:((uparrow y) `),([#] x):] \/ [:([#] T),((uparrow J2) `):] is Element of bool the carrier of [:T,x:]

AA is Element of the carrier of W

uparrow AA is non empty filtered upper Element of bool the carrier of W

{AA} is non empty finite compact Element of bool the carrier of W

uparrow {AA} is non empty upper Element of bool the carrier of W

(uparrow AA) ` is lower Element of bool the carrier of W

the carrier of W \ (uparrow AA) is set

z is V69(W) quasi_prebasis Element of bool (bool the carrier of W)

[#] y9 is non empty non proper open closed dense non boundary filtered lower upper inaccessible_by_directed_joins closed_under_directed_sups Element of bool the carrier of y9

a is Element of the carrier of y9

uparrow a is non empty filtered upper Element of bool the carrier of y9

{a} is non empty finite compact Element of bool the carrier of y9

uparrow {a} is non empty upper Element of bool the carrier of y9

(uparrow a) ` is lower Element of bool the carrier of y9

the carrier of y9 \ (uparrow a) is set

G is Element of bool the carrier of [:y9,W:]

G is Element of bool the carrier of [:y9,W:]

G \/ G is Element of bool the carrier of [:y9,W:]

z is V69(W) quasi_prebasis Element of bool (bool the carrier of W)

{ [: the carrier of y9,b

{ [: the carrier of y9,b

UniCl the topology of [:y9,W:] is Element of bool (bool the carrier of [:y9,W:])

I2 is V69([:y9,W:]) quasi_prebasis Element of bool (bool the carrier of [:y9,W:])

Y is set

Z is Element of bool the carrier of W

[: the carrier of y9,Z:] is set

J2 is Element of the carrier of W

uparrow J2 is non empty filtered upper Element of bool the carrier of W

{J2} is non empty finite compact Element of bool the carrier of W

uparrow {J2} is non empty upper Element of bool the carrier of W

(uparrow J2) ` is lower Element of bool the carrier of W

the carrier of W \ (uparrow J2) is set

Bottom T is Element of the carrier of T

y is Element of the carrier of x

[(Bottom T),y] is Element of the carrier of [:T,x:]

{(Bottom T),y} is non empty finite set

{(Bottom T)} is non empty finite set

{{(Bottom T),y},{(Bottom T)}} is non empty finite V32() set

a is Element of the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric non void () TopAugmentation of [:T,x:]

uparrow a is non empty filtered upper Element of bool the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric non void () TopAugmentation of [:T,x:]

{a} is non empty finite compact Element of bool the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric non void () TopAugmentation of [:T,x:]

uparrow {a} is non empty upper Element of bool the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric non void () TopAugmentation of [:T,x:]

uparrow [(Bottom T),y] is non empty filtered upper Element of bool the carrier of [:T,x:]

{[(Bottom T),y]} is non empty finite Element of bool the carrier of [:T,x:]

uparrow {[(Bottom T),y]} is non empty upper Element of bool the carrier of [:T,x:]

uparrow (Bottom T) is non empty filtered upper Element of bool the carrier of T

bool the carrier of T is non empty set

{(Bottom T)} is non empty finite Element of bool the carrier of T

uparrow {(Bottom T)} is non empty upper Element of bool the carrier of T

(uparrow (Bottom T)) ` is lower Element of bool the carrier of T

the carrier of T \ (uparrow (Bottom T)) is set

uparrow y is non empty filtered upper Element of bool the carrier of x

bool the carrier of x is non empty set

{y} is non empty finite Element of bool the carrier of x

uparrow {y} is non empty upper Element of bool the carrier of x

(uparrow [(Bottom T),y]) ` is lower Element of bool the carrier of [:T,x:]

the carrier of [:T,x:] \ (uparrow [(Bottom T),y]) is set

[:{}, the carrier of x:] is set

[: the carrier of T,Z:] is set

[:{}, the carrier of x:] \/ [: the carrier of T,Z:] is set

{} \/ [: the carrier of T,Z:] is set

Z is Element of bool the carrier of y9

[:Z, the carrier of W:] is set

J2 is Element of the carrier of y9

uparrow J2 is non empty filtered upper Element of bool the carrier of y9

{J2} is non empty finite compact Element of bool the carrier of y9

uparrow {J2} is non empty upper Element of bool the carrier of y9

(uparrow J2) ` is lower Element of bool the carrier of y9

the carrier of y9 \ (uparrow J2) is set

y is Element of the carrier of T

Bottom x is Element of the carrier of x

[y,(Bottom x)] is Element of the carrier of [:T,x:]

{y,(Bottom x)} is non empty finite set

{y} is non empty finite set

{{y,(Bottom x)},{y}} is non empty finite V32() set

a is Element of the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric non void () TopAugmentation of [:T,x:]

uparrow a is non empty filtered upper Element of bool the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric non void () TopAugmentation of [:T,x:]

{a} is non empty finite compact Element of bool the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric non void () TopAugmentation of [:T,x:]

uparrow {a} is non empty upper Element of bool the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric non void () TopAugmentation of [:T,x:]

uparrow [y,(Bottom x)] is non empty filtered upper Element of bool the carrier of [:T,x:]

{[y,(Bottom x)]} is non empty finite Element of bool the carrier of [:T,x:]

uparrow {[y,(Bottom x)]} is non empty upper Element of bool the carrier of [:T,x:]

uparrow (Bottom x) is non empty filtered upper Element of bool the carrier of x

bool the carrier of x is non empty set

{(Bottom x)} is non empty finite Element of bool the carrier of x

uparrow {(Bottom x)} is non empty upper Element of bool the carrier of x

(uparrow (Bottom x)) ` is lower Element of bool the carrier of x

the carrier of x \ (uparrow (Bottom x)) is set

uparrow y is non empty filtered upper Element of bool the carrier of T

bool the carrier of T is non empty set

{y} is non empty finite Element of bool the carrier of T

uparrow {y} is non empty upper Element of bool the carrier of T

(uparrow [y,(Bottom x)]) ` is lower Element of bool the carrier of [:T,x:]

the carrier of [:T,x:] \ (uparrow [y,(Bottom x)]) is set

[:Z, the carrier of x:] is set

[: the carrier of T,{}:] is set

[:Z, the carrier of x:] \/ [: the carrier of T,{}:] is set

[:Z, the carrier of x:] \/ {} is set

FinMeetCl I2 is Element of bool (bool the carrier of [:y9,W:])

FinMeetCl x9 is Element of bool (bool the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric non void () TopAugmentation of [:T,x:])

UniCl (FinMeetCl I2) is Element of bool (bool the carrier of [:y9,W:])

UniCl (FinMeetCl x9) is Element of bool (bool the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric non void () TopAugmentation of [:T,x:])

the topology of the non empty TopSpace-like T_0 reflexive transitive antisymmetric non void () TopAugmentation of [:T,x:] is non empty Element of bool (bool the carrier of the non empty TopSpace-like T_0 reflexive transitive antisymmetric non void () TopAugmentation of [:T,x:])

FinMeetCl the topology of [:y9,W:] is Element of bool (bool the carrier of [:y9,W:])

T is non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded non void () TopRelStr

x is non empty TopSpace-like T_0 reflexive transitive antisymmetric lower-bounded non void () TopRelStr

[:T,x:] is non empty strict reflexive transitive antisymmetric non void RelStr

([:T,x:]) is Element of bool (bool the carrier of [:T,x:])

the carrier of [:T,x:] is non empty set

bool the carrier of [:T,x:] is non empty set

bool (bool the carrier of [:T,x:]) is non empty set

[:T,x:] is non empty strict TopSpace-like TopStruct

the topology of [:T,x:] is non empty Element of bool (bool the carrier of [:T,x:])

the carrier of [:T,x:] is non empty set

bool the carrier of [:T,x:] is non empty set

bool (bool the carrier of [:T,x:]) is non empty set

x is non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete non void () TopRelStr

T is non empty TopSpace-like T_0 reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete non void () TopRelStr

[:T,T:] is non empty strict reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V196() up-complete /\-complete non void RelStr

the carrier of x is non empty set

the carrier of T is non empty set

[: the carrier of x, the carrier of T:] is non empty set

bool [: the carrier of x, the carrier of T:] is non empty set

inf_op T is Relation-like the carrier of [:T,T:] -defined the carrier of T -valued Function-like V18( the carrier of [:T,T:], the carrier of T) infs-preserving meet-preserving filtered-infs-preserving Element of bool [: the carrier of [:T,T:], the carrier of T:]

the carrier of [:T,T:] is non empty set

[: the carrier of [:T,T:], the carrier of T:] is non empty set

bool [: the carrier of [:T,T:], the carrier of T:] is non empty set

the InternalRel of x is non empty Relation-like the carrier of x -defined the carrier of x -valued Element of bool [: the carrier of x, the carrier of x:]

[: the carrier of x, the carrier of x:] is non empty set

bool [: the carrier of x, the carrier of x:] is non empty set

RelStr(# the carrier of x, the InternalRel of x #) is strict RelStr

the InternalRel of [:T,T:] is non empty Relation-like the carrier of [:T,T:] -defined the carrier of [:T,T:] -valued Element of bool [: the carrier of [:T,T:], the carrier of [:T,T:]:]

[: the carrier of [:T,T:], the carrier of [:T,T:]:] is non empty set

bool [: the carrier of [:T,T:], the carrier of [:T,T:]:] is non empty set

RelStr(# the carrier of [:T,T:], the InternalRel of [:T,T:] #) is strict RelStr

y is Relation-like the carrier of x -defined the carrier of T -valued Function-like V18( the carrier of x, the carrier of T) Element of bool [: the carrier of x, the carrier of T:]

bool the carrier of x is non empty set

x9 is Element of bool the carrier of x

bool the carrier of [:T,T:] is non empty set

y .: x9 is Element of bool the carrier of T

bool the carrier of T is non empty set

"/\" ((y .: x9),T) is Element of the carrier of T

"/\" (x9,x) is Element of the carrier of x

K76( the carrier of x, the carrier of T,y,("/\" (x9,x))) is Element of the carrier of T

y9 is Element of bool the carrier of [:T,T:]

"/\" (y9,[:T,T:]) is Element of the carrier of [:T,T:]

(inf_op T) . ("/\" (y9,[:T,T:])) is Element of the carrier of T

y . ("/\" (x9,x)) is Element of the carrier of T

F

the carrier of F

bool the carrier of F

bool (bool the carrier of F

[#] F

T is V69(F

T is V69(F

x is Element of bool the carrier of F

the topology of F

FinMeetCl T is Element of bool (bool the carrier of F

UniCl (FinMeetCl T) is Element of bool (bool the carrier of F

y is Element of bool (bool the carrier of F

union y is Element of bool the carrier of F

y9 is Element of bool the carrier of F

x9 is Element of bool (bool the carrier of F

u is Element of bool (bool the carrier of F

Intersect u is Element of bool the carrier of F

W is set

V is set

{W} is non empty finite set

V \/ {W} is non empty set

x is Element of bool (bool the carrier of F

z is Element of bool (bool the carrier of F

Y is Element of bool (bool the carrier of F

I2 is Element of bool (bool the carrier of F

Z is Element of bool (bool the carrier of F

Intersect Z is Element of bool the carrier of F

y is Element of bool the carrier of F

a is Element of bool (bool the carrier of F

Intersect a is Element of bool the carrier of F

Y is Element of bool (bool the carrier of F

Intersect Y is Element of bool the carrier of F

J2 is Element of bool the carrier of F

J2 /\ y is Element of bool the carrier of F

W is Element of bool (bool the carrier of F

Intersect W is Element of bool the carrier of F

T is non empty reflexive antisymmetric up-complete non void RelStr

the carrier of T is non empty set

the InternalRel of T is non empty Relation-like the carrier of T -defined the carrier of T -valued Element of bool [: the carrier of T, the carrier of T:]

[: the carrier of T, the carrier of T:] is non empty set

bool [: the carrier of T, the carrier of T:] is non empty set

RelStr(# the carrier of T, the InternalRel of T #) is strict RelStr

x is non empty reflexive antisymmetric up-complete non void RelStr

the carrier of x is non empty set

the InternalRel of x is non empty Relation-like the carrier of x -defined the carrier of x -valued Element of bool [: the carrier of x, the carrier of x:]

[: the carrier of x, the carrier of x:] is non empty set

bool [: the carrier of x, the carrier of x:] is non empty set

RelStr(# the carrier of x, the InternalRel of x #) is strict RelStr

y is Element of the carrier of x

waybelow y is Element of bool the carrier of x

bool the carrier of x is non empty set

{ b

"\/" ((waybelow y),x) is Element of the carrier of x

x9 is Element of the carrier of T

waybelow x9 is Element of bool the carrier of T

bool the carrier of T is non empty set

{ b

"\/" ((waybelow x9),T) is Element of the carrier of T

T is non empty reflexive transitive antisymmetric satisfying_axiom_of_approximation continuous up-complete non void RelStr

x is non empty reflexive transitive antisymmetric non void TopAugmentation of T

the carrier of x is non empty set

the InternalRel of x is non empty Relation-like the carrier of x -defined the carrier of x -valued Element of bool [: the carrier of x, the carrier of x:]

[: the carrier of x, the carrier of x:] is non empty set

bool [: the carrier of x, the carrier of x:] is non empty set

RelStr(# the carrier of x, the InternalRel of x #) is strict RelStr

the carrier of T is non empty set

the InternalRel of T is non empty Relation-like the carrier of T -defined the carrier of T -valued Element of bool [: the carrier of T, the carrier of T:]

[: the carrier of T, the carrier of T:] is non empty set

bool [: the carrier of T, the carrier of T:] is non empty set

RelStr(# the carrier of T, the InternalRel of T #) is strict RelStr

T is TopSpace-like TopStruct

x is TopSpace-like TopStruct

the topology of T is non empty Element of bool (bool the carrier of T)

the carrier of T is set

bool the carrier of T is non empty set

bool (bool the carrier of T) is non empty set

the topology of x is non empty Element of bool (bool the carrier of x)

the carrier of x is set

bool the carrier of x is non empty set

bool (bool the carrier of x) is non empty set

y is TopSpace-like Refinement of T,x

the carrier of y is set

bool the carrier of y is non empty set

x9 is Element of bool the carrier of y

the topology of T \/ the topology of x is non empty set

bool (bool the carrier of y) is non empty set

the topology of y is non empty Element of bool (bool the carrier of y)

T is TopSpace-like TopStruct

x is TopSpace-like TopStruct

the carrier of T is set

bool the carrier of T is non empty set

y is TopSpace-like Refinement of T,x

the carrier of y is set

bool the carrier of y is non empty set

x9 is Element of bool the carrier of T

y9 is Element of bool the carrier of y

the topology of T is non empty Element of bool (bool the carrier of T)

bool (bool the carrier of T) is non empty set

T is TopSpace-like TopStruct

the carrier of T is set

x is TopSpace-like TopStruct

the carrier of x is set

bool the carrier of T is non empty set

y is TopSpace-like Refinement of T,x

the carrier of y is set

bool the carrier of y is non empty set

x9 is Element of bool the carrier of T

y9 is Element of bool the carrier of y

x9 ` is Element of bool the carrier of T

the carrier of T \ x9 is set

the carrier of T \/ the carrier of x is set

y9 ` is Element of bool the carrier of y

the carrier of y \ y9 is set

the topology of T is non empty Element of bool (bool the carrier of T)

bool (bool the carrier of T) is non empty set

T is non empty TopSpace-like TopStruct

the topology of T is non empty Element of bool (bool the carrier of T)

the carrier of T is non empty set

bool the carrier of T is non empty set

bool (bool the carrier of T) is non empty set

x is set

y is set

x9 is Element of bool (bool the carrier of T)

y9 is Element of bool (bool the carrier of T)

u is Element of bool (bool the carrier of T)

W is Element of bool (bool the carrier of T)

V is Element of bool (bool the carrier of T)

UniCl V is Element of bool (bool the carrier of T)

x is Element of bool (bool the carrier of T)

UniCl x is Element of bool (bool the carrier of T)

UniCl the topology of T is Element of bool (bool the carrier of T)

FinMeetCl the topology of T is Element of bool (bool the carrier of T)

FinMeetCl x is Element of bool (bool the carrier of T)

UniCl (FinMeetCl x) is Element of bool (bool the carrier of T)

FinMeetCl V is Element of bool (bool the carrier of T)

UniCl (FinMeetCl V) is Element of bool (bool the carrier of T)

T is non empty TopSpace-like TopStruct

the carrier of T is non empty set

x is non empty TopSpace-like TopStruct

the carrier of x is non empty set

bool the carrier of T is non empty set

bool (bool the carrier of T) is non empty set

bool the carrier of x is non empty set

bool (bool the carrier of x) is non empty set

y is non empty TopSpace-like Refinement of T,x

the carrier of y is non empty set

bool the carrier of y is non empty set

bool (bool the carrier of y) is non empty set

x9 is V69(T) quasi_prebasis Element of bool (bool the carrier of T)

y9 is V69(x) quasi_prebasis Element of bool (bool the carrier of x)

x9 \/ y9 is set

the carrier of T \/ the carrier of x is non empty set

{ the carrier of T, the carrier of x} is non empty finite set

{ the carrier of y} is non empty finite set

(x9 \/ y9) \/ { the carrier of y} is non empty set

u is V69(y) quasi_prebasis Element of bool (bool the carrier of y)

W is Element of bool (bool the carrier of y)

FinMeetCl W is Element of bool (bool the carrier of y)

V is set

FinMeetCl u is Element of bool (bool the carrier of y)

FinMeetCl (FinMeetCl W) is Element of bool (bool the carrier of y)

T is non empty TopSpace-like TopStruct

x is non empty TopSpace-like TopStruct

y is non empty TopSpace-like TopStruct

x9 is non empty TopSpace-like TopStruct

the carrier of T is non empty set

the carrier of y is non empty set

[: the carrier of T, the carrier of y:] is non empty set

bool [: the carrier of T, the carrier of y:] is non empty set

the carrier of x is non empty set

the carrier of x9 is non empty set

[: the carrier of x, the carrier of x9:] is non empty set

bool [: the carrier of x, the carrier of x9:] is non empty set

y9 is non empty TopSpace-like Refinement of T,x

the carrier of y9 is non empty set

u is non empty TopSpace-like Refinement of y,x9

the carrier of u is non empty set

[: the carrier of y9, the carrier of u:] is non empty set

bool [: the carrier of y9, the carrier of u:] is non empty set

W is Relation-like the carrier of T -defined the carrier of y -valued Function-like V18( the carrier of T, the carrier of y) Element of bool [: the carrier of T, the carrier of y:]

V is Relation-like the carrier of x -defined the carrier of x9 -valued Function-like V18( the carrier of x, the carrier of x9) Element of bool [: the carrier of x, the carrier of x9:]

x is Relation-like the carrier of y9 -defined the carrier of u -valued Function-like V18( the carrier of y9, the carrier of u) Element of bool [: the carrier of y9, the carrier of u:]

[#] x9 is non empty non proper open closed dense non boundary Element of bool the carrier of x9

bool the carrier of x9 is non empty set

bool the carrier of u is non empty set

bool (bool the carrier of u) is non empty set

the topology of y is non empty Element of bool (bool the carrier of y)

bool the carrier of y is non empty set

bool (bool the carrier of y) is non empty set

the topology of x9 is non empty Element of bool (bool the carrier of x9)

bool (bool the carrier of x9) is non empty set

the topology of y \/ the topology of x9 is non empty set

[#] y is non empty non proper open closed dense non boundary Element of bool the carrier of y

Y is Element of bool the carrier of u

z is V69(u) quasi_prebasis Element of bool (bool the carrier of u)

I2 is Element of bool the carrier of y

W " I2 is Element of bool the carrier of T

bool the carrier of T is non empty set

x " Y is Element of bool the carrier of y9

bool the carrier of y9 is non empty set

I2 is Element of bool the carrier of x9

V " I2 is Element of bool the carrier of x

bool the carrier of x is non empty set

x " Y is Element of bool the carrier of y9

bool the carrier of y9 is non empty set

T is non empty TopSpace-like TopStruct

the carrier of T is non empty set

bool the carrier of T is non empty set

bool (bool the carrier of T) is non empty set

x is V69(T) quasi_prebasis Element of bool (bool the carrier of T)

y is non empty transitive directed NetStr over T

Lim y is Element of bool the carrier of T

x9 is Element of the carrier of T

the carrier of y is non empty set

y9 is a_neighborhood of x9

Int y9 is open Element of bool the carrier of T

the topology of T is non empty Element of bool (