:: WAYBEL12 semantic presentation

REAL is set

NAT is non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal countable denumerable Element of bool REAL

bool REAL is non empty cup-closed diff-closed preBoolean set

{} is empty V10() non-empty empty-yielding functional ext-real epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V39() V40() finite finite-yielding V47() cardinal {} -element countable FinSequence-like FinSequence-membered set

the empty V10() non-empty empty-yielding functional ext-real epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V39() V40() finite finite-yielding V47() cardinal {} -element countable FinSequence-like FinSequence-membered set is empty V10() non-empty empty-yielding functional ext-real epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V39() V40() finite finite-yielding V47() cardinal {} -element countable FinSequence-like FinSequence-membered set

COMPLEX is set

omega is non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal countable denumerable set

bool omega is non empty non trivial cup-closed diff-closed preBoolean non finite set

bool NAT is non empty non trivial cup-closed diff-closed preBoolean non finite set

1 is non empty ext-real epsilon-transitive epsilon-connected ordinal natural V39() V40() finite cardinal countable Element of NAT

2 is non empty ext-real epsilon-transitive epsilon-connected ordinal natural V39() V40() finite cardinal countable Element of NAT

3 is non empty ext-real epsilon-transitive epsilon-connected ordinal natural V39() V40() finite cardinal countable Element of NAT

card omega is non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal set

0 is empty V10() non-empty empty-yielding functional ext-real epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V39() V40() finite finite-yielding V47() cardinal {} -element countable FinSequence-like FinSequence-membered Element of NAT

T is non empty RelStr

the carrier of T is non empty set

[:NAT, the carrier of T:] is non empty non trivial V10() non finite set

bool [:NAT, the carrier of T:] is non empty non trivial cup-closed diff-closed preBoolean non finite set

bool the carrier of T is non empty cup-closed diff-closed preBoolean set

F is V10() V13( NAT ) V14( the carrier of T) Function-like V21( NAT , the carrier of T) Element of bool [:NAT, the carrier of T:]

I is ext-real epsilon-transitive epsilon-connected ordinal natural V39() V40() finite cardinal countable Element of NAT

{ (F . b

{0} is non empty trivial finite V47() 1 -element countable Element of bool NAT

Seg I is finite I -element countable Element of bool NAT

{0} \/ (Seg I) is non empty finite countable Element of bool NAT

{ (F . b

S is set

p is ext-real epsilon-transitive epsilon-connected ordinal natural V39() V40() finite cardinal countable Element of NAT

F . p is Element of the carrier of T

Seg p is finite p -element countable Element of bool NAT

S is set

p is ext-real epsilon-transitive epsilon-connected ordinal natural V39() V40() finite cardinal countable Element of NAT

F . p is Element of the carrier of T

{ H

card { H

card ({0} \/ (Seg I)) is non empty ext-real epsilon-transitive epsilon-connected ordinal natural V39() V40() finite cardinal countable Element of omega

F . 0 is Element of the carrier of T

T is TopStruct

the carrier of T is set

bool the carrier of T is non empty cup-closed diff-closed preBoolean set

F is Element of bool the carrier of T

F ` is Element of bool the carrier of T

the carrier of T \ F is set

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

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

T is TopStruct

the carrier of T is set

bool the carrier of T is non empty cup-closed diff-closed preBoolean set

bool (bool the carrier of T) is non empty cup-closed diff-closed preBoolean set

T is set

card T is epsilon-transitive epsilon-connected ordinal cardinal set

F is set

card F is epsilon-transitive epsilon-connected ordinal cardinal set

T is non trivial non finite countable denumerable set

card T is non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal set

card NAT is non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal set

T is non empty transitive RelStr

the carrier of T is non empty set

bool the carrier of T is non empty cup-closed diff-closed preBoolean set

F is Element of bool the carrier of T

I is Element of bool the carrier of T

downarrow F is lower Element of bool the carrier of T

downarrow I is lower Element of bool the carrier of T

Q is set

S is Element of the carrier of T

p is Element of the carrier of T

Y is Element of the carrier of T

T is non empty transitive RelStr

the carrier of T is non empty set

bool the carrier of T is non empty cup-closed diff-closed preBoolean set

I is Element of bool the carrier of T

F is Element of bool the carrier of T

uparrow F is upper Element of bool the carrier of T

uparrow I is upper Element of bool the carrier of T

Q is set

S is Element of the carrier of T

p is Element of the carrier of T

Y is Element of the carrier of T

T is non empty reflexive transitive antisymmetric RelStr

the carrier of T is non empty set

bool the carrier of T is non empty cup-closed diff-closed preBoolean set

F is non empty finite filtered countable Element of bool the carrier of T

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

I is Element of the carrier of T

T is non empty antisymmetric lower-bounded RelStr

the carrier of T is non empty set

bool the carrier of T is non empty cup-closed diff-closed preBoolean set

Bottom T is Element of the carrier of T

F is non empty lower Element of bool the carrier of T

I is set

Q is Element of F

T is non empty antisymmetric lower-bounded RelStr

the carrier of T is non empty set

bool the carrier of T is non empty cup-closed diff-closed preBoolean set

Bottom T is Element of the carrier of T

F is non empty Element of bool the carrier of T

downarrow F is Element of bool the carrier of T

I is set

{ b

( b

Q is Element of F

T is non empty antisymmetric upper-bounded RelStr

the carrier of T is non empty set

bool the carrier of T is non empty cup-closed diff-closed preBoolean set

Top T is Element of the carrier of T

F is non empty upper Element of bool the carrier of T

I is set

Q is Element of F

T is non empty antisymmetric upper-bounded RelStr

the carrier of T is non empty set

bool the carrier of T is non empty cup-closed diff-closed preBoolean set

Top T is Element of the carrier of T

F is non empty Element of bool the carrier of T

uparrow F is Element of bool the carrier of T

I is set

{ b

( b

Q is Element of F

T is non empty antisymmetric lower-bounded with_infima RelStr

the carrier of T is non empty set

bool the carrier of T is non empty cup-closed diff-closed preBoolean set

Bottom T is Element of the carrier of T

{(Bottom T)} is non empty trivial finite 1 -element countable Element of bool the carrier of T

F is Element of bool the carrier of T

F "/\" {(Bottom T)} is Element of bool the carrier of T

{ (b

{(Bottom T)} "/\" F is Element of bool the carrier of T

{ (b

{ ((Bottom T) "/\" b

I is set

Q is Element of the carrier of T

(Bottom T) "/\" Q is Element of the carrier of T

Q "/\" (Bottom T) is Element of the carrier of T

T is non empty antisymmetric lower-bounded with_infima RelStr

the carrier of T is non empty set

bool the carrier of T is non empty cup-closed diff-closed preBoolean set

Bottom T is Element of the carrier of T

{(Bottom T)} is non empty trivial finite 1 -element countable Element of bool the carrier of T

F is non empty Element of bool the carrier of T

F "/\" {(Bottom T)} is non empty Element of bool the carrier of T

{ (b

I is set

{ ((Bottom T) "/\" b

Q is set

S is Element of F

(Bottom T) "/\" S is Element of the carrier of T

T is non empty antisymmetric upper-bounded with_suprema RelStr

the carrier of T is non empty set

bool the carrier of T is non empty cup-closed diff-closed preBoolean set

Top T is Element of the carrier of T

{(Top T)} is non empty trivial finite 1 -element countable Element of bool the carrier of T

F is Element of bool the carrier of T

F "\/" {(Top T)} is Element of bool the carrier of T

{ (b

{(Top T)} "\/" F is Element of bool the carrier of T

{ (b

{ ((Top T) "\/" b

I is set

Q is Element of the carrier of T

(Top T) "\/" Q is Element of the carrier of T

Q "\/" (Top T) is Element of the carrier of T

T is non empty antisymmetric upper-bounded with_suprema RelStr

the carrier of T is non empty set

bool the carrier of T is non empty cup-closed diff-closed preBoolean set

Top T is Element of the carrier of T

{(Top T)} is non empty trivial finite 1 -element countable Element of bool the carrier of T

F is non empty Element of bool the carrier of T

F "\/" {(Top T)} is non empty Element of bool the carrier of T

{ (b

I is set

{ ((Top T) "\/" b

Q is set

S is Element of F

(Top T) "\/" S is Element of the carrier of T

T is non empty reflexive transitive antisymmetric upper-bounded with_infima RelStr

the carrier of T is non empty set

bool the carrier of T is non empty cup-closed diff-closed preBoolean set

Top T is Element of the carrier of T

{(Top T)} is non empty trivial finite 1 -element countable Element of bool the carrier of T

F is Element of bool the carrier of T

{(Top T)} "/\" F is Element of bool the carrier of T

{ (b

{ ((Top T) "/\" b

I is set

Q is Element of the carrier of T

(Top T) "/\" Q is Element of the carrier of T

I is set

Q is non empty Element of bool the carrier of T

S is Element of Q

(Top T) "/\" S is Element of the carrier of T

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

the carrier of T is non empty set

bool the carrier of T is non empty cup-closed diff-closed preBoolean set

Bottom T is Element of the carrier of T

{(Bottom T)} is non empty trivial finite 1 -element countable Element of bool the carrier of T

F is Element of bool the carrier of T

{(Bottom T)} "\/" F is Element of bool the carrier of T

{ (b

{ ((Bottom T) "\/" b

I is set

Q is Element of the carrier of T

(Bottom T) "\/" Q is Element of the carrier of T

I is set

Q is non empty Element of bool the carrier of T

S is Element of Q

(Bottom T) "\/" S is Element of the carrier of T

T is non empty reflexive RelStr

the carrier of T is non empty set

bool the carrier of T is non empty cup-closed diff-closed preBoolean set

F is Element of bool the carrier of T

I is Element of bool the carrier of T

Q is Element of the carrier of T

S is Element of the carrier of T

Q is Element of the carrier of T

S is Element of the carrier of T

T is non empty transitive antisymmetric with_infima RelStr

the carrier of T is non empty set

bool the carrier of T is non empty cup-closed diff-closed preBoolean set

F is Element of bool the carrier of T

I is Element of the carrier of T

Q is Element of the carrier of T

{I} is non empty trivial finite 1 -element countable Element of bool the carrier of T

{I} "/\" F is Element of bool the carrier of T

{ (b

{Q} is non empty trivial finite 1 -element countable Element of bool the carrier of T

{Q} "/\" F is Element of bool the carrier of T

{ (b

{ (Q "/\" b

S is Element of the carrier of T

p is Element of the carrier of T

Q "/\" p is Element of the carrier of T

I "/\" p is Element of the carrier of T

Y is Element of the carrier of T

{ (I "/\" b

T is non empty transitive antisymmetric with_suprema RelStr

the carrier of T is non empty set

bool the carrier of T is non empty cup-closed diff-closed preBoolean set

F is Element of bool the carrier of T

I is Element of the carrier of T

Q is Element of the carrier of T

{I} is non empty trivial finite 1 -element countable Element of bool the carrier of T

{I} "\/" F is Element of bool the carrier of T

{ (b

{Q} is non empty trivial finite 1 -element countable Element of bool the carrier of T

{Q} "\/" F is Element of bool the carrier of T

{ (b

{ (I "\/" b

S is Element of the carrier of T

p is Element of the carrier of T

I "\/" p is Element of the carrier of T

Q "\/" p is Element of the carrier of T

Y is Element of the carrier of T

{ (Q "\/" b

T is non empty RelStr

the carrier of T is non empty set

bool the carrier of T is non empty cup-closed diff-closed preBoolean set

Q is Element of bool the carrier of T

I is Element of bool the carrier of T

F is Element of bool the carrier of T

S is set

p is non empty Element of bool the carrier of T

Y is Element of p

Y1 is Element of the carrier of T

T is non empty RelStr

the carrier of T is non empty set

bool the carrier of T is non empty cup-closed diff-closed preBoolean set

I is Element of bool the carrier of T

Q is Element of bool the carrier of T

F is Element of bool the carrier of T

S is set

p is non empty Element of bool the carrier of T

Y is Element of p

Y1 is Element of the carrier of T

T is non empty reflexive transitive antisymmetric with_infima RelStr

the carrier of T is non empty set

bool the carrier of T is non empty cup-closed diff-closed preBoolean set

F is filtered upper Element of bool the carrier of T

F "/\" F is filtered Element of bool the carrier of T

{ (b

I is set

Q is Element of the carrier of T

S is Element of the carrier of T

Q "/\" S is Element of the carrier of T

p is Element of the carrier of T

T is non empty reflexive transitive antisymmetric with_suprema RelStr

the carrier of T is non empty set

bool the carrier of T is non empty cup-closed diff-closed preBoolean set

F is directed lower Element of bool the carrier of T

F "\/" F is directed Element of bool the carrier of T

{ (b

I is set

Q is Element of the carrier of T

S is Element of the carrier of T

Q "\/" S is Element of the carrier of T

p is Element of the carrier of T

T is non empty RelStr

the carrier of T is non empty set

bool the carrier of T is non empty cup-closed diff-closed preBoolean set

F is Element of bool the carrier of T

{ b

Q is set

S is Element of the carrier of T

{S} is non empty trivial finite 1 -element countable Element of bool the carrier of T

F "/\" {S} is Element of bool the carrier of T

{ (b

T is non empty reflexive transitive antisymmetric upper-bounded with_infima RelStr

the carrier of T is non empty set

bool the carrier of T is non empty cup-closed diff-closed preBoolean set

F is Element of bool the carrier of T

{ b

Top T is Element of the carrier of T

{(Top T)} is non empty trivial finite 1 -element countable Element of bool the carrier of T

F "/\" {(Top T)} is Element of bool the carrier of T

{ (b

T is non empty transitive antisymmetric with_infima RelStr

the carrier of T is non empty set

bool the carrier of T is non empty cup-closed diff-closed preBoolean set

F is Element of bool the carrier of T

{ b

I is Element of bool the carrier of T

Q is Element of the carrier of T

S is Element of the carrier of T

p is Element of the carrier of T

{p} is non empty trivial finite 1 -element countable Element of bool the carrier of T

F "/\" {p} is Element of bool the carrier of T

{ (b

Y is Element of the carrier of T

{Y} is non empty trivial finite 1 -element countable Element of bool the carrier of T

F "/\" {Y} is Element of bool the carrier of T

{ (b

p "/\" Y is Element of the carrier of T

Y1 is Element of the carrier of T

{Y1} is non empty trivial finite 1 -element countable Element of bool the carrier of T

F "/\" {Y1} is Element of bool the carrier of T

{ (b

{Y1} "/\" F is Element of bool the carrier of T

{ (b

{ (Y1 "/\" b

A is set

q is Element of the carrier of T

Y1 "/\" q is Element of the carrier of T

{p} "/\" F is Element of bool the carrier of T

{ (b

{ (p "/\" b

Y "/\" q is Element of the carrier of T

p "/\" (Y "/\" q) is Element of the carrier of T

{Y} "/\" F is Element of bool the carrier of T

{ (b

{ (Y "/\" b

T is non empty transitive antisymmetric with_infima RelStr

the carrier of T is non empty set

bool the carrier of T is non empty cup-closed diff-closed preBoolean set

F is upper Element of bool the carrier of T

{ b

I is Element of bool the carrier of T

Q is Element of the carrier of T

S is Element of the carrier of T

{S} is non empty trivial finite 1 -element countable Element of bool the carrier of T

F "/\" {S} is Element of bool the carrier of T

{ (b

p is Element of the carrier of T

{p} is non empty trivial finite 1 -element countable Element of bool the carrier of T

F "/\" {p} is Element of bool the carrier of T

{ (b

T is non empty reflexive transitive antisymmetric with_infima RelStr

the carrier of T is non empty set

bool the carrier of T is non empty cup-closed diff-closed preBoolean set

F is Element of bool the carrier of T

I is Element of the carrier of T

Q is Element of the carrier of T

I "/\" Q is Element of the carrier of T

S is Element of the carrier of T

T is non empty reflexive transitive antisymmetric with_infima RelStr

the carrier of T is non empty set

bool the carrier of T is non empty cup-closed diff-closed preBoolean set

F is Element of bool the carrier of T

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

the carrier of T is non empty set

bool the carrier of T is non empty cup-closed diff-closed preBoolean set

F is Element of bool the carrier of T

I is Element of the carrier of T

waybelow I is non empty directed Element of bool the carrier of T

Q is set

S is Element of the carrier of T

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

the carrier of T is non empty set

F is Element of the carrier of T

downarrow F is non empty directed filtered lower Open Element of bool the carrier of T

bool the carrier of T is non empty cup-closed diff-closed preBoolean set

{F} is non empty trivial finite 1 -element countable Element of bool the carrier of T

downarrow {F} is non empty filtered lower Open Element of bool the carrier of T

(downarrow F) ` is upper Element of bool the carrier of T

the carrier of T \ (downarrow F) is set

I is Element of the carrier of T

S is Element of the carrier of T

waybelow S is non empty directed filtered lower Open Element of bool the carrier of T

p is Element of the carrier of T

waybelow p is non empty directed filtered lower Open Element of bool the carrier of T

S is Element of the carrier of T

T is non empty reflexive transitive antisymmetric with_infima RelStr

the carrier of T is non empty set

bool the carrier of T is non empty cup-closed diff-closed preBoolean set

F is non empty Element of bool the carrier of T

bool F is non empty cup-closed diff-closed preBoolean set

Fin F is non empty cup-closed diff-closed preBoolean set

I is non empty finite countable Element of Fin F

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

Q is non empty finite countable Element of Fin F

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

I \/ Q is non empty finite countable Element of Fin F

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

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

I is non empty finite countable Element of bool F

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

Q is Element of F

{Q} is non empty trivial finite 1 -element countable Element of bool F

"/\" ({Q},T) is Element of the carrier of T

T is non empty reflexive transitive antisymmetric with_suprema RelStr

the carrier of T is non empty set

bool the carrier of T is non empty cup-closed diff-closed preBoolean set

F is non empty Element of bool the carrier of T

bool F is non empty cup-closed diff-closed preBoolean set

Fin F is non empty cup-closed diff-closed preBoolean set

I is non empty finite countable Element of Fin F

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

Q is non empty finite countable Element of Fin F

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

I \/ Q is non empty finite countable Element of Fin F

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

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

I is non empty finite countable Element of bool F

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

Q is Element of F

{Q} is non empty trivial finite 1 -element countable Element of bool F

"\/" ({Q},T) is Element of the carrier of T

T is non empty reflexive transitive antisymmetric with_infima RelStr

the carrier of T is non empty set

bool the carrier of T is non empty cup-closed diff-closed preBoolean set

F is non empty filtered upper Element of bool the carrier of T

fininfs F is non empty filtered Element of bool the carrier of T

bool F is non empty cup-closed diff-closed preBoolean set

{ ("/\" (b

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

T is non empty reflexive transitive antisymmetric with_infima RelStr

the carrier of T is non empty set

bool the carrier of T is non empty cup-closed diff-closed preBoolean set

F is non empty filtered upper Element of bool the carrier of T

fininfs F is non empty filtered Element of bool the carrier of T

bool F is non empty cup-closed diff-closed preBoolean set

{ ("/\" (b

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

T is non empty reflexive transitive antisymmetric with_infima RelStr

the carrier of T is non empty set

bool the carrier of T is non empty cup-closed diff-closed preBoolean set

F is non empty filtered upper Element of bool the carrier of T

fininfs F is non empty filtered Element of bool the carrier of T

bool F is non empty cup-closed diff-closed preBoolean set

{ ("/\" (b

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

I is (T,F)

T is non empty reflexive transitive antisymmetric with_infima RelStr

the carrier of T is non empty set

bool the carrier of T is non empty cup-closed diff-closed preBoolean set

F is non empty filtered upper Element of bool the carrier of T

I is (T,F)

fininfs I is filtered Element of bool the carrier of T

bool I is non empty cup-closed diff-closed preBoolean set

{ ("/\" (b

uparrow (fininfs I) is filtered upper Element of bool the carrier of T

T is non empty reflexive transitive antisymmetric with_infima RelStr

the carrier of T is non empty set

bool the carrier of T is non empty cup-closed diff-closed preBoolean set

F is Element of bool the carrier of T

fininfs F is filtered Element of bool the carrier of T

bool F is non empty cup-closed diff-closed preBoolean set

{ ("/\" (b

I is non empty Element of bool the carrier of T

fininfs I is non empty filtered Element of bool the carrier of T

bool I is non empty cup-closed diff-closed preBoolean set

{ ("/\" (b

Q is Element of the carrier of T

S is finite countable Element of bool F

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

p is set

Y is Element of the carrier of T

Y1 is Element of the carrier of T

[:S,I:] is V10() set

bool [:S,I:] is non empty cup-closed diff-closed preBoolean set

p is V10() V13(S) V14(I) Function-like V21(S,I) finite countable Element of bool [:S,I:]

p .: S is finite countable Element of bool I

Y is set

dom p is finite countable Element of bool S

bool S is non empty cup-closed diff-closed preBoolean finite V47() countable set

Y1 is set

p . Y1 is set

Y is set

dom p is finite countable Element of bool S

bool S is non empty cup-closed diff-closed preBoolean finite V47() countable set

p . Y is set

"/\" ((p .: S),T) is Element of the carrier of T

Y is Element of the carrier of T

p . Y is set

Y1 is Element of the carrier of T

A is Element of the carrier of T

dom p is finite countable Element of bool S

bool S is non empty cup-closed diff-closed preBoolean finite V47() countable set

T is non empty reflexive transitive antisymmetric with_infima RelStr

the carrier of T is non empty set

bool the carrier of T is non empty cup-closed diff-closed preBoolean set

F is non empty filtered upper Element of bool the carrier of T

I is (T,F)

Q is non empty Element of bool the carrier of T

fininfs I is filtered Element of bool the carrier of T

bool I is non empty cup-closed diff-closed preBoolean set

{ ("/\" (b

uparrow (fininfs I) is filtered upper Element of bool the carrier of T

fininfs Q is non empty filtered Element of bool the carrier of T

bool Q is non empty cup-closed diff-closed preBoolean set

{ ("/\" (b

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

T is non empty reflexive transitive antisymmetric with_infima RelStr

the carrier of T is non empty set

bool the carrier of T is non empty cup-closed diff-closed preBoolean set

[:NAT, the carrier of T:] is non empty non trivial V10() non finite set

bool [:NAT, the carrier of T:] is non empty non trivial cup-closed diff-closed preBoolean non finite set

F is Element of bool the carrier of T

I is V10() V13( NAT ) V14( the carrier of T) Function-like V21( NAT , the carrier of T) Element of bool [:NAT, the carrier of T:]

rng I is Element of bool the carrier of T

Q is V10() V13( NAT ) V14( the carrier of T) Function-like V21( NAT , the carrier of T) Element of bool [:NAT, the carrier of T:]

rng Q is Element of bool the carrier of T

S is Element of the carrier of T

dom I is countable Element of bool NAT

p is set

I . p is set

Y is ext-real epsilon-transitive epsilon-connected ordinal natural V39() V40() finite cardinal countable Element of NAT

{ (I . b

Y1 is non empty finite countable Element of bool the carrier of T

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

A is Element of the carrier of T

dom Q is countable Element of bool NAT

Q . Y is Element of the carrier of T

I . Y is Element of the carrier of T

{(I . Y)} is non empty trivial finite 1 -element countable Element of bool the carrier of T

"/\" ({(I . Y)},T) is Element of the carrier of T

T is non empty reflexive transitive antisymmetric with_infima RelStr

the carrier of T is non empty set

bool the carrier of T is non empty cup-closed diff-closed preBoolean set

[:NAT, the carrier of T:] is non empty non trivial V10() non finite set

bool [:NAT, the carrier of T:] is non empty non trivial cup-closed diff-closed preBoolean non finite set

F is non empty filtered upper Element of bool the carrier of T

I is (T,F)

Q is V10() V13( NAT ) V14( the carrier of T) Function-like V21( NAT , the carrier of T) Element of bool [:NAT, the carrier of T:]

rng Q is Element of bool the carrier of T

S is V10() V13( NAT ) V14( the carrier of T) Function-like V21( NAT , the carrier of T) Element of bool [:NAT, the carrier of T:]

rng S is Element of bool the carrier of T

p is Element of the carrier of T

dom S is countable Element of bool NAT

Y is set

S . Y is set

Y1 is ext-real epsilon-transitive epsilon-connected ordinal natural V39() V40() finite cardinal countable Element of NAT

{ (Q . b

A is non empty finite countable Element of bool the carrier of T

q is set

dom Q is countable Element of bool NAT

p is ext-real epsilon-transitive epsilon-connected ordinal natural V39() V40() finite cardinal countable Element of NAT

Q . p is Element of the carrier of T

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

S . Y1 is Element of the carrier of T

S . 0 is Element of the carrier of T

T is non empty reflexive transitive antisymmetric lower-bounded upper-bounded bounded up-complete /\-complete with_suprema with_infima V175() satisfying_axiom_of_approximation continuous RelStr

the carrier of T is non empty set

bool the carrier of T is non empty cup-closed diff-closed preBoolean set

F is upper Open Element of bool the carrier of T

I is non empty filtered upper Element of bool the carrier of T

F "/\" I is Element of bool the carrier of T

{ (b

Q is Element of the carrier of T

S is non empty upper Open Element of bool the carrier of T

{ b

Y1 is non empty (T,I)

[:NAT,Y1:] is non empty non trivial V10() non finite set

bool [:NAT,Y1:] is non empty non trivial cup-closed diff-closed preBoolean non finite set

A is V10() V13( NAT ) V14(Y1) Function-like V21( NAT ,Y1) Element of bool [:NAT,Y1:]

rng A is Element of bool Y1

bool Y1 is non empty cup-closed diff-closed preBoolean set

[:NAT, the carrier of T:] is non empty non trivial V10() non finite set

bool [:NAT, the carrier of T:] is non empty non trivial cup-closed diff-closed preBoolean non finite set

q is V10() V13( NAT ) V14( the carrier of T) Function-like V21( NAT , the carrier of T) Element of bool [:NAT, the carrier of T:]

{ (q . b

"/\" ( { (q . b

p is V10() V13( NAT ) V14( the carrier of T) Function-like V21( NAT , the carrier of T) Element of bool [:NAT, the carrier of T:]

dom p is countable Element of bool NAT

rng p is Element of bool the carrier of T

P is non empty Element of bool the carrier of T

Y is non empty filtered upper Element of bool the carrier of T

A is set

V is Element of the carrier of T

{V} is non empty trivial finite 1 -element countable Element of bool the carrier of T

F "/\" {V} is Element of bool the carrier of T

{ (b

{ (V "/\" b

v is set

x is Element of the carrier of T

V "/\" x is Element of the carrier of T

x "/\" V is Element of the carrier of T

A is ext-real epsilon-transitive epsilon-connected ordinal natural V39() V40() finite cardinal countable Element of NAT

A + 1 is ext-real epsilon-transitive epsilon-connected ordinal natural V39() V40() finite cardinal countable Element of NAT

p . (A + 1) is Element of the carrier of T

V is Element of S

v is Element of the carrier of T

{v} is non empty trivial finite 1 -element countable Element of bool the carrier of T

F "/\" {v} is Element of bool the carrier of T

{ (b

V "/\" v is Element of the carrier of T

x is Element of the carrier of T

[:NAT,S:] is non empty non trivial V10() non finite set

bool [:NAT,S:] is non empty non trivial cup-closed diff-closed preBoolean non finite set

p is Element of S

A is V10() V13( NAT ) V14(S) Function-like V21( NAT ,S) Element of bool [:NAT,S:]

A . 0 is Element of S

dom A is countable Element of bool NAT

rng A is Element of bool S

bool S is non empty cup-closed diff-closed preBoolean set

V is non empty Element of bool the carrier of T

fininfs V is non empty filtered Element of bool the carrier of T

bool V is non empty cup-closed diff-closed preBoolean set

{ ("/\" (b

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

x is Element of the carrier of T

x is Element of the carrier of T

q is ext-real epsilon-transitive epsilon-connected ordinal natural V39() V40() finite cardinal countable Element of NAT

A . q is Element of S

q + 1 is ext-real epsilon-transitive epsilon-connected ordinal natural V39() V40() finite cardinal countable Element of NAT

A . (q + 1) is Element of S

p . (q + 1) is Element of the carrier of T

y is Element of S

Y is Element of S

n is Element of the carrier of T

y "/\" n is Element of the carrier of T

x is ext-real epsilon-transitive epsilon-connected ordinal natural V39() V40() finite cardinal countable Element of NAT

A . x is Element of S

x + 1 is ext-real epsilon-transitive epsilon-connected ordinal natural V39() V40() finite cardinal countable Element of NAT

A . (x + 1) is Element of S

q is ext-real epsilon-transitive epsilon-connected ordinal natural V39() V40() finite cardinal countable Element of NAT

A . q is Element of S

Y is Element of the carrier of T

y is Element of the carrier of T

x is Element of the carrier of T

q is Element of the carrier of T

x is ext-real epsilon-transitive epsilon-connected ordinal natural V39() V40() finite cardinal countable Element of NAT

A . x is Element of S

x is Element of the carrier of T

x is Element of the carrier of T

x is Element of the carrier of T

q is ext-real epsilon-transitive epsilon-connected ordinal natural V39() V40() finite cardinal countable Element of NAT

A . q is Element of S

y is ext-real epsilon-transitive epsilon-connected ordinal natural V39() V40() finite cardinal countable Element of NAT

A . y is Element of S

x is Element of the carrier of T

x is Element of the carrier of T

q is set

A . q is set

Y is set

A . Y is set

y is ext-real epsilon-transitive epsilon-connected ordinal natural V39() V40() finite cardinal countable Element of NAT

n is ext-real epsilon-transitive epsilon-connected ordinal natural V39() V40() finite cardinal countable Element of NAT

n is ext-real epsilon-transitive epsilon-connected ordinal natural V39() V40() finite cardinal countable Element of NAT

y is ext-real epsilon-transitive epsilon-connected ordinal natural V39() V40() finite cardinal countable Element of NAT

y is ext-real epsilon-transitive epsilon-connected ordinal natural V39() V40() finite cardinal countable Element of NAT

n is ext-real epsilon-transitive epsilon-connected ordinal natural V39() V40() finite cardinal countable Element of NAT

x is Element of the carrier of T

x is Element of the carrier of T

q is finite countable Element of bool V

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

y is set

A . y is set

Y is ext-real epsilon-transitive epsilon-connected ordinal natural V39() V40() finite cardinal countable Element of NAT

A . Y is Element of S

Y + 1 is ext-real epsilon-transitive epsilon-connected ordinal natural V39() V40() finite cardinal countable Element of NAT

A . (Y + 1) is Element of S

p . (Y + 1) is Element of the carrier of T

n is Element of S

n is Element of S

x1 is Element of the carrier of T

n "/\" x1 is Element of the carrier of T

y is set

Y is Element of the carrier of T

n is set

A . n is set

Top T is Element of the carrier of T

n is ext-real epsilon-transitive epsilon-connected ordinal natural V39() V40() finite cardinal countable Element of NAT

A . n is Element of S

n + 1 is ext-real epsilon-transitive epsilon-connected ordinal natural V39() V40() finite cardinal countable Element of NAT

A . (n + 1) is Element of S

p . (n + 1) is Element of the carrier of T

x1 is Element of S

y1 is Element of S

z1 is Element of the carrier of T

x1 "/\" z1 is Element of the carrier of T

x is ext-real epsilon-transitive epsilon-connected ordinal natural V39() V40() finite cardinal countable Element of NAT

p . x is Element of the carrier of T

x + 1 is ext-real epsilon-transitive epsilon-connected ordinal natural V39() V40() finite cardinal countable Element of NAT

p . (x + 1) is Element of the carrier of T

x is Element of the carrier of T

q is Element of the carrier of T

{ (q . b

{ (q . b

y is non empty finite countable Element of bool the carrier of T

Y is non empty finite countable Element of bool the carrier of T

n is set

n is ext-real epsilon-transitive epsilon-connected ordinal natural V39() V40() finite cardinal countable Element of NAT

q . n is Element of the carrier of T

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

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

x is Element of the carrier of T

x is set

p . x is set

q is ext-real epsilon-transitive epsilon-connected ordinal natural V39() V40() finite cardinal countable Element of NAT

A . q is Element of S

q + 1 is ext-real epsilon-transitive epsilon-connected ordinal natural V39() V40() finite cardinal countable Element of NAT

A . (q + 1) is Element of S

p . (q + 1) is Element of the carrier of T

y is Element of S

Y is Element of S

n is Element of the carrier of T

y "/\" n is Element of the carrier of T

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

x is set

q is Element of x

y is Element of the carrier of T

Y is finite countable Element of bool V

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

n is set

A . n is set

n is ext-real epsilon-transitive epsilon-connected ordinal natural V39() V40() finite cardinal countable Element of NAT

A . n is Element of S

n + 1 is ext-real epsilon-transitive epsilon-connected ordinal natural V39() V40() finite cardinal countable Element of NAT

A . (n + 1) is Element of S

p . (n + 1) is Element of the carrier of T

x1 is Element of S

y1 is Element of S

z1 is Element of the carrier of T

x1 "/\" z1 is Element of the carrier of T

Top T is Element of the carrier of T

fininfs P is non empty filtered Element of bool the carrier of T

bool P is non empty cup-closed diff-closed preBoolean set

{ ("/\" (b

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

T is non empty reflexive transitive antisymmetric lower-bounded upper-bounded bounded up-complete /\-complete with_suprema with_infima V175() satisfying_axiom_of_approximation continuous RelStr

the carrier of T is non empty set

bool the carrier of T is non empty cup-closed diff-closed preBoolean set

F is upper Open Element of bool the carrier of T

I is non empty countable Element of bool the carrier of T

F "/\" I is Element of bool the carrier of T

{ (b

Q is Element of the carrier of T

{Q} is non empty trivial finite 1 -element countable Element of bool the carrier of T

{Q} "/\" I is non empty Element of bool the carrier of T

{ (b

{ b

S is non empty filtered upper Element of bool the carrier of T

p is set

Y is Element of the carrier of T

{Y} is non empty trivial finite 1 -element countable Element of bool the carrier of T

{Y} "/\" F is Element of bool the carrier of T

{ (b

{ (Y "/\" b

F "/\" {Y} is Element of bool the carrier of T

{ (b

Y1 is set

A is Element of the carrier of T

Y "/\" A is Element of the carrier of T

I "/\" F is Element of bool the carrier of T

{ (b

fininfs I is non empty filtered Element of bool the carrier of T

bool I is non empty cup-closed diff-closed preBoolean set

{ ("/\" (b

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

p is non empty filtered upper Element of bool the carrier of T

F "/\" p is Element of bool the carrier of T

{ (b

Y is set

Y1 is Element of the carrier of T

A is Element of the carrier of T

Y1 "/\" A is Element of the carrier of T

q is Element of the carrier of T

{q} is non empty trivial finite 1 -element countable Element of bool the carrier of T

F "/\" {q} is Element of bool the carrier of T

{ (b

Y is non empty filtered upper Open Element of bool the carrier of T

{ (Q "/\" b

Y1 is set

A is Element of the carrier of T

Q "/\" A is Element of the carrier of T

Y "/\" Y is non empty filtered Element of bool the carrier of T

{ (b

T is non empty reflexive transitive antisymmetric lower-bounded upper-bounded bounded up-complete /\-complete with_suprema with_infima V175() satisfying_axiom_of_approximation continuous RelStr

the carrier of T is non empty set

bool the carrier of T is non empty cup-closed diff-closed preBoolean set

F is upper Open Element of bool the carrier of T

I is non empty countable Element of bool the carrier of T

F "/\" I is Element of bool the carrier of T

{ (b

S is Element of the carrier of T

Q is Element of the carrier of T

{S} is non empty trivial finite 1 -element countable Element of bool the carrier of T

{S} "/\" I is non empty Element of bool the carrier of T

{ (b

uparrow ({S} "/\" I) is non empty upper Element of bool the carrier of T

p is non empty filtered upper Open Element of bool the carrier of T

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

p ` is filtered lower Open Element of bool the carrier of T

the carrier of T \ p is set

Y is Element of the carrier of T

Y1 is meet-irreducible Element of the carrier of T

T is non empty reflexive transitive antisymmetric lower-bounded upper-bounded bounded up-complete /\-complete with_suprema with_infima V175() satisfying_axiom_of_approximation continuous RelStr

the carrier of T is non empty set

bool the carrier of T is non empty cup-closed diff-closed preBoolean set

F is Element of the carrier of T

I is non empty countable Element of bool the carrier of T

downarrow F is non empty directed filtered lower Open Element of bool the carrier of T

{F} is non empty trivial finite 1 -element countable Element of bool the carrier of T

downarrow {F} is non empty filtered lower Open Element of bool the carrier of T

(downarrow F) ` is upper Open Element of bool the carrier of T

the carrier of T \ (downarrow F) is set

((downarrow F) `) "/\" I is Element of bool the carrier of T

{ (b

S is set

p is Element of the carrier of T

Y is Element of the carrier of T

p "/\" Y is Element of the carrier of T

S is Element of the carrier of T

{S} is non empty trivial finite 1 -element countable Element of bool the carrier of T

{S} "/\" I is non empty Element of bool the carrier of T

{ (b

uparrow ({S} "/\" I) is non empty upper Element of bool the carrier of T

T is non empty RelStr

the carrier of T is non empty set

T is non empty reflexive transitive antisymmetric upper-bounded with_infima RelStr

Top T is Element of the carrier of T

the carrier of T is non empty set

F is Element of the carrier of T

Bottom T is Element of the carrier of T

(Top T) "/\" F is Element of the carrier of T

(Top T) "/\" F is Element of the carrier of T

T is non empty reflexive transitive antisymmetric upper-bounded with_infima RelStr

the carrier of T is non empty set

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

T is non empty non trivial reflexive transitive antisymmetric lower-bounded upper-bounded bounded with_infima RelStr

the carrier of T is non empty non trivial set

Bottom T is Element of the carrier of T

F is Element of the carrier of T

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

F "/\" (Top T) is Element of the carrier of T

T is non empty RelStr

the carrier of T is non empty set

bool the carrier of T is non empty cup-closed diff-closed preBoolean set

T is non empty reflexive transitive antisymmetric upper-bounded with_infima RelStr

the carrier of T is non empty set

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

{(Top T)} is non empty trivial finite 1 -element countable Element of bool the carrier of T

bool the carrier of T is non empty cup-closed diff-closed preBoolean set

F is Element of the carrier of T

T is non empty reflexive transitive antisymmetric upper-bounded with_infima RelStr

the carrier of T is non empty set

bool the carrier of T is non empty cup-closed diff-closed preBoolean set

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

{(Top T)} is non empty trivial finite 1 -element countable Element of bool the carrier of T

T is non empty reflexive transitive antisymmetric lower-bounded upper-bounded bounded up-complete /\-complete with_suprema with_infima V175() satisfying_axiom_of_approximation continuous RelStr

the carrier of T is non empty set

bool the carrier of T is non empty cup-closed diff-closed preBoolean set

Bottom T is Element of the carrier of T

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

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

I is Element of the carrier of T

{I} is non empty trivial finite 1 -element countable Element of bool the carrier of T

{I} "/\" F is non empty Element of bool the carrier of T

{ (b

uparrow ({I} "/\" F) is non empty upper Element of bool the carrier of T

S is Element of the carrier of T

Q is Element of the carrier of T

S "/\" Q is Element of the carrier of T

Q is meet-irreducible Element of the carrier of T

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 cup-closed diff-closed preBoolean set

bool (bool the carrier of T) is non empty cup-closed diff-closed preBoolean set

InclPoset the topology of T is non empty non trivial strict reflexive transitive antisymmetric lower-bounded upper-bounded bounded up-complete /\-complete with_suprema with_infima V175() RelStr

the carrier of (InclPoset the topology of T) is non empty non trivial set

F is Element of the carrier of (InclPoset the topology of T)

I is Element of bool the carrier of T

I ` is Element of bool the carrier of T

the carrier of T \ I is set

Q is Element of the carrier of (InclPoset the topology of T)

S is Element of the carrier of (InclPoset the topology of T)

Q "/\" S is Element of the carrier of (InclPoset the topology of T)

Q "/\" S is Element of the carrier of (InclPoset the topology of T)

Y is Element of bool the carrier of T

Y ` is Element of bool the carrier of T

the carrier of T \ Y is set

p is Element of bool the carrier of T

p /\ Y is Element of bool the carrier of T

Q /\ S is set

p ` is Element of bool the carrier of T

the carrier of T \ p is set

(p `) \/ (Y `) is Element of bool the carrier of T

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 cup-closed diff-closed preBoolean set

bool (bool the carrier of T) is non empty cup-closed diff-closed preBoolean set

InclPoset the topology of T is non empty non trivial strict reflexive transitive antisymmetric lower-bounded upper-bounded bounded up-complete /\-complete with_suprema with_infima V175() RelStr

the carrier of (InclPoset the topology of T) is non empty non trivial set

Top (InclPoset the topology of T) is ( InclPoset the topology of T) Element of the carrier of (InclPoset the topology of T)

F is Element of the carrier of (InclPoset the topology of T)

I is Element of bool the carrier of T

I ` is Element of bool the carrier of T

the carrier of T \ I is set

the carrier of T \ I is Element of bool the carrier of T

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

the carrier of T \ (I `) is set

Q is Element of bool the carrier of T

S is Element of bool the carrier of T

Q \/ S is Element of bool the carrier of T

Q ` is Element of bool the carrier of T

the carrier of T \ Q is set

S ` is Element of bool the carrier of T

the carrier of T \ S is set

(Q `) /\ (S `) is Element of bool the carrier of T

p is Element of the carrier of (InclPoset the topology of T)

Y is Element of the carrier of (InclPoset the topology of T)

p /\ Y is set

(Q \/ S) ` is Element of bool the carrier of T

the carrier of T \ (Q \/ S) is set

p "/\" Y is Element of the carrier of (InclPoset the topology of T)

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 cup-closed diff-closed preBoolean set

bool (bool the carrier of T) is non empty cup-closed diff-closed preBoolean set

InclPoset the topology of T is non empty non trivial strict reflexive transitive antisymmetric lower-bounded upper-bounded bounded up-complete /\-complete with_suprema with_infima V175() RelStr

the carrier of (InclPoset the topology of T) is non empty non trivial set

F is Element of the carrier of (InclPoset the topology of T)

I is Element of bool the carrier of T

Bottom (InclPoset the topology of T) is Element of the carrier of (InclPoset the topology of T)

Q is Element of bool the carrier of T

I /\ Q is Element of bool the carrier of T

S is Element of the carrier of (InclPoset the topology of T)

F /\ S is set

F "/\" S is Element of the carrier of (InclPoset the topology of T)

Q is Element of the carrier of (InclPoset the topology of T)

F "/\" Q is Element of the carrier of (InclPoset the topology of T)

S is Element of bool the carrier of T

I /\ S is Element of bool the carrier of T

F "/\" Q is Element of the carrier of (InclPoset the topology of T)

T is non empty TopSpace-like TopStruct

the carrier of T is non empty set

bool the carrier of T is non empty cup-closed diff-closed preBoolean set

bool (bool the carrier of T) is non empty cup-closed diff-closed preBoolean set

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

InclPoset the topology of T is non empty non trivial strict reflexive transitive antisymmetric lower-bounded upper-bounded bounded up-complete /\-complete with_suprema with_infima V175() RelStr

F is non empty reflexive transitive antisymmetric lower-bounded upper-bounded bounded up-complete /\-complete with_suprema with_infima V175() satisfying_axiom_of_approximation continuous RelStr

the carrier of F is non empty set

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

Q is set

S is Element of bool the carrier of T

{ b

( b

Y1 is set

A is Element of the carrier of F

q is Element of bool the carrier of T

bool the carrier of F is non empty cup-closed diff-closed preBoolean set

Y1 is Element of bool the carrier of F

A is set

q is Element of the carrier of F

p is Element of bool the carrier of T

A is Element of the carrier of F

q is Element of the carrier of F

p is Element of bool the carrier of T

A is non empty Element of bool the carrier of T

p is Element of the carrier of F

q is Element of the carrier of F

Bottom F is Element of the carrier of F

Top F is (F) Element of the carrier of F

{q} is non empty trivial finite 1 -element countable Element of bool the carrier of F

{q} "/\" Y1 is Element of bool the carrier of F

{ (b

uparrow ({q} "/\" Y1) is upper Element of bool the carrier of F

p is meet-irreducible Element of the carrier of F

P is Element of bool the carrier of T

P ` is Element of bool the carrier of T

the carrier of T \ P is set

A is non empty irreducible Element of bool the carrier of T

A /\ A is Element of bool the carrier of T

V is Element of bool the carrier of T

x is Element of the carrier of F

q "/\" x is Element of the carrier of F

v is Element of the carrier of F

q "/\" v is Element of the carrier of F

A /\ V is Element of bool the carrier of T

q /\ v is set

A ` is Element of bool the carrier of T

the carrier of T \ A is set

x is set

x is Element of the carrier of T

(A /\ V) /\ A is Element of bool the carrier of T

(A /\ A) /\ V is Element of bool the carrier of T

T is non empty TopSpace-like TopStruct

the carrier of T is non empty set

bool the carrier of T is non empty cup-closed diff-closed preBoolean set

bool (bool the carrier of T) is non empty cup-closed diff-closed preBoolean set

bool the carrier of T is non empty cup-closed diff-closed preBoolean Element of bool (bool the carrier of T)

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

Intersect I is Element of bool the carrier of T

Q is Element of bool the carrier of T

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

Intersect I is Element of bool the carrier of T

{ (Int b

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

bool [:(bool the carrier of T),(bool the carrier of T):] is non empty cup-closed diff-closed preBoolean set

S is V10() V13( bool the carrier of T) V14( bool the carrier of T) Function-like V21( bool the carrier of T, bool the carrier of T) Element of bool [:(bool the carrier of T),(bool the carrier of T):]

S .: I is Element of bool (bool the carrier of T)

bool (bool the carrier of T) is non empty cup-closed diff-closed preBoolean set

p is set

Y is Element of bool the carrier of T

Int Y is open Element of bool the carrier of T

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

S . Y is Element of bool the carrier of T

card { (Int b

card I is epsilon-transitive epsilon-connected ordinal cardinal set

Y is set

Y1 is Element of bool the carrier of T

Int Y1 is open Element of bool the carrier of T

p is Element of bool the carrier of T

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

Intersect Y is Element of bool the carrier of T

Y1 is set

A is Element of bool the carrier of T

Int A is open Element of bool the carrier of T

q is set

Y1 is Element of bool the carrier of T

A is Element of bool the carrier of T

Int A is open Element of bool the carrier of T

Y1 is Element of bool the carrier of T

T is non empty TopSpace-like TopStruct

the carrier of T is non empty set

bool the carrier of T is non empty cup-closed diff-closed preBoolean set

bool (bool the carrier of T) is non empty cup-closed diff-closed preBoolean set

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

Intersect F is Element of bool the carrier of T

I is Element of bool the carrier of T

I is Element of bool the carrier of T

I is Element of bool the carrier of T

Q is Element of bool the carrier of T

S is non empty irreducible Element of bool the carrier of T

S /\ Q is Element of bool the carrier of T

p is Element of the carrier of T

{p} is non empty trivial finite 1 -element countable Element of bool the carrier of T

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

Y is set

Y1 is Element of bool the carrier of T

(S /\ Q) /\ Y1 is Element of bool the carrier of T

Q /\ Y1 is Element of bool the carrier of T

(Q /\ Y1) ` is Element of bool the carrier of T

the carrier of T \ (Q /\ Y1) is set

Cl ((Q /\ Y1) `) is closed Element of bool the carrier of T

S /\ (Q /\ Y1) is Element of bool the carrier of T

Y is set

Y is set

(Intersect F) /\ Q is Element of bool the carrier of T

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