:: YELLOW13 semantic presentation

K182() is set

K186() is non empty non trivial V24() V25() V26() non finite V36() V37() Element of bool K182()

bool K182() is non empty set

K96() is non empty non trivial V24() V25() V26() non finite V36() V37() set

bool K96() is non empty non trivial non finite set

K179() is non empty strict TopSpace-like TopStruct

the carrier of K179() is non empty set

bool K186() is non empty non trivial non finite set

{} is empty V7() non-empty empty-yielding V24() V25() V26() V28() V29() V30() finite finite-yielding V35() V36() V38( {} ) set

the empty V7() non-empty empty-yielding V24() V25() V26() V28() V29() V30() finite finite-yielding V35() V36() V38( {} ) set is empty V7() non-empty empty-yielding V24() V25() V26() V28() V29() V30() finite finite-yielding V35() V36() V38( {} ) set

1 is non empty V24() V25() V26() V30() finite V36() Element of K186()

{{},1} is non empty finite V35() set

T is non empty TopSpace-like T_0 T_1 TopStruct

the carrier of T is non empty set

bool the carrier of T is non empty set

x is finite Element of bool the carrier of T

{} T is empty proper V7() non-empty empty-yielding V24() V25() V26() V28() V29() V30() finite finite-yielding V35() V36() V38( {} ) open closed boundary nowhere_dense Element of bool the carrier of T

p is set

G is set

{p} is non empty trivial finite V38(1) set

G \/ {p} is non empty set

xp is Element of bool the carrier of T

xp is Element of bool the carrier of T

TT is Element of the carrier of T

{TT} is non empty trivial finite V38(1) compact Element of bool the carrier of T

xp \/ {TT} is non empty Element of bool the carrier of T

p is Element of bool the carrier of T

T is non empty TopSpace-like T_0 T_1 TopStruct

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

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

the carrier of T is set

bool the carrier of T 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

x is Element of bool the carrier of T

T is TopSpace-like TopStruct

the carrier of T is set

T is non empty TopSpace-like discrete almost_discrete extremally_disconnected hereditarily_extremally_disconnected TopStruct

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

p is Element of bool the carrier of T

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

G is Element of bool the carrier of T

TT is Element of bool the carrier of T

G /\ TT is Element of bool the carrier of T

T is non empty TopSpace-like discrete almost_discrete extremally_disconnected hereditarily_extremally_disconnected TopStruct

the carrier of T is non empty set

bool the carrier of T is non empty set

x is Element of the carrier of T

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

{x} is non empty trivial finite V38(1) compact Element of bool the carrier of T

G is non empty trivial finite V38(1) compact Element of bool the carrier of T

TT is Element of bool the carrier of T

G /\ TT is finite Element of bool the carrier of T

xp is set

T is non empty TopSpace-like discrete almost_discrete extremally_disconnected hereditarily_extremally_disconnected TopStruct

the carrier of T is non empty set

x is Element of the carrier of T

p is Element of the carrier of T

bool the carrier of T is non empty set

{x} is non empty trivial finite V38(1) compact Element of bool the carrier of T

G is non empty trivial finite V38(1) compact Element of bool the carrier of T

{p} is non empty trivial finite V38(1) compact Element of bool the carrier of T

TT is non empty trivial finite V38(1) compact Element of bool the carrier of T

G /\ TT is finite Element of bool the carrier of T

xp is set

T is non empty TopSpace-like discrete almost_discrete extremally_disconnected hereditarily_extremally_disconnected TopStruct

the carrier of T is non empty set

x is Element of the carrier of T

{x} is non empty trivial finite V38(1) compact Element of bool the carrier of T

bool the carrier of T is non empty set

T is TopSpace-like TopStruct

T is non empty TopSpace-like TopStruct

the carrier of T is non empty set

bool the carrier of T is non empty set

x is Element of the carrier of T

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

{x} is non empty trivial finite V38(1) compact Element of bool the carrier of T

p /\ {x} is finite Element of bool the carrier of T

G is set

G is Element of bool the carrier of T

TT is Element of bool the carrier of T

T is TopSpace-like TopStruct

the carrier of T is set

x is Element of the carrier of T

p is Element of the carrier of T

bool the carrier of T is non empty set

{p} is non empty trivial finite V38(1) set

G is non empty TopSpace-like TopStruct

the carrier of G is non empty set

TT is Element of the carrier of G

xp is Element of the carrier of G

{xp} is non empty trivial finite V38(1) compact Element of bool the carrier of G

bool the carrier of G is non empty set

{xp} ` is Element of bool the carrier of G

the carrier of G \ {xp} is set

f is Element of bool the carrier of T

H is Element of bool the carrier of T

T is reflexive RelStr

the carrier of T is set

bool the carrier of T is non empty set

x is reflexive transitive RelStr

the carrier of x is set

[: the carrier of T, the carrier of x:] is V7() set

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

p is V7() V10( the carrier of T) V11( the carrier of x) Function-like quasi_total Element of bool [: the carrier of T, the carrier of x:]

G is Element of bool the carrier of T

p .: G is Element of bool the carrier of x

bool the carrier of x is non empty set

downarrow (p .: G) is Element of bool the carrier of x

downarrow G is Element of bool the carrier of T

p .: (downarrow G) is Element of bool the carrier of x

downarrow (p .: (downarrow G)) is Element of bool the carrier of x

T is reflexive RelStr

the carrier of T is set

bool the carrier of T is non empty set

x is reflexive transitive RelStr

the carrier of x is set

[: the carrier of T, the carrier of x:] is V7() set

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

p is V7() V10( the carrier of T) V11( the carrier of x) Function-like quasi_total Element of bool [: the carrier of T, the carrier of x:]

G is Element of bool the carrier of T

p .: G is Element of bool the carrier of x

bool the carrier of x is non empty set

downarrow (p .: G) is Element of bool the carrier of x

downarrow G is Element of bool the carrier of T

p .: (downarrow G) is Element of bool the carrier of x

downarrow (p .: (downarrow G)) is Element of bool the carrier of x

TT is set

xp is non empty reflexive transitive RelStr

the carrier of xp is non empty set

f is Element of the carrier of xp

H is Element of the carrier of xp

dom p is Element of bool the carrier of T

A is set

p . A is set

Z is non empty reflexive RelStr

the carrier of Z is non empty set

X1 is Element of the carrier of Z

Y1 is Element of the carrier of Z

[: the carrier of Z, the carrier of xp:] is non empty V7() set

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

Y1 is V7() V10( the carrier of Z) V11( the carrier of xp) Function-like quasi_total Element of bool [: the carrier of Z, the carrier of xp:]

Y1 . X1 is Element of the carrier of xp

Y1 . Y1 is Element of the carrier of xp

p . Y1 is set

T is non empty reflexive transitive antisymmetric RelStr

IdsMap T is V7() V10( the carrier of T) V11( the carrier of (InclPoset (Ids T))) Function-like quasi_total monotone Element of bool [: the carrier of T, the carrier of (InclPoset (Ids T)):]

the carrier of T is non empty set

Ids T is non empty set

bool the carrier of T is non empty set

{ b

InclPoset (Ids T) is non empty strict reflexive transitive antisymmetric RelStr

the carrier of (InclPoset (Ids T)) is non empty set

[: the carrier of T, the carrier of (InclPoset (Ids T)):] is non empty V7() set

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

p is Element of the carrier of T

(IdsMap T) . p is Element of the carrier of (InclPoset (Ids T))

G is Element of the carrier of T

(IdsMap T) . G is Element of the carrier of (InclPoset (Ids T))

downarrow p is non empty directed lower Element of bool the carrier of T

{p} is non empty trivial finite V38(1) Element of bool the carrier of T

downarrow {p} is non empty lower Element of bool the carrier of T

downarrow G is non empty directed lower Element of bool the carrier of T

{G} is non empty trivial finite V38(1) Element of bool the carrier of T

downarrow {G} is non empty lower Element of bool the carrier of T

T is non empty reflexive transitive antisymmetric RelStr

IdsMap T is V7() V10( the carrier of T) V11( the carrier of (InclPoset (Ids T))) Function-like quasi_total monotone Element of bool [: the carrier of T, the carrier of (InclPoset (Ids T)):]

the carrier of T is non empty set

Ids T is non empty set

bool the carrier of T is non empty set

{ b

InclPoset (Ids T) is non empty strict reflexive transitive antisymmetric RelStr

the carrier of (InclPoset (Ids T)) is non empty set

[: the carrier of T, the carrier of (InclPoset (Ids T)):] is non empty V7() set

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

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

SupMap T is V7() V10( the carrier of (InclPoset (Ids T))) V11( the carrier of T) Function-like quasi_total monotone Element of bool [: the carrier of (InclPoset (Ids T)), the carrier of T:]

Ids T is non empty set

the carrier of T is non empty finite set

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

{ b

InclPoset (Ids T) is non empty strict reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V192() up-complete /\-complete RelStr

the carrier of (InclPoset (Ids T)) is non empty set

[: the carrier of (InclPoset (Ids T)), the carrier of T:] is non empty V7() set

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

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

(SupMap T) . p is Element of the carrier of T

G is Element of the carrier of (InclPoset (Ids T))

(SupMap T) . G is Element of the carrier of T

TT is non empty finite directed lower Element of bool the carrier of T

sup TT is Element of the carrier of T

xp is non empty finite directed lower Element of bool the carrier of T

sup xp is Element of the carrier of T

f is set

H is Element of the carrier of T

f is set

H is Element of the carrier of T

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

SupMap T is V7() V10( the carrier of (InclPoset (Ids T))) V11( the carrier of T) Function-like quasi_total monotone Element of bool [: the carrier of (InclPoset (Ids T)), the carrier of T:]

Ids T is non empty set

the carrier of T is non empty finite set

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

{ b

InclPoset (Ids T) is non empty strict reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V192() up-complete /\-complete RelStr

the carrier of (InclPoset (Ids T)) is non empty set

[: the carrier of (InclPoset (Ids T)), the carrier of T:] is non empty V7() set

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

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

Ids T is non empty set

the carrier of T is non empty finite set

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

{ b

InclPoset (Ids T) is non empty strict reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded V192() up-complete /\-complete RelStr

the carrier of (InclPoset (Ids T)) is non empty set

[: the carrier of T, the carrier of (InclPoset (Ids T)):] is non empty V7() set

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

IdsMap T is V7() V10( the carrier of T) V11( the carrier of (InclPoset (Ids T))) Function-like one-to-one quasi_total finite monotone Element of bool [: the carrier of T, the carrier of (InclPoset (Ids T)):]

p is V7() V10( the carrier of T) V11( the carrier of (InclPoset (Ids T))) Function-like one-to-one quasi_total finite monotone Element of bool [: the carrier of T, the carrier of (InclPoset (Ids T)):]

[: the carrier of (InclPoset (Ids T)), the carrier of T:] is non empty V7() set

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

p " is V7() Function-like set

SupMap T is V7() V10( the carrier of (InclPoset (Ids T))) V11( the carrier of T) Function-like one-to-one quasi_total monotone Element of bool [: the carrier of (InclPoset (Ids T)), the carrier of T:]

G is V7() V10( the carrier of (InclPoset (Ids T))) V11( the carrier of T) Function-like one-to-one quasi_total monotone Element of bool [: the carrier of (InclPoset (Ids T)), the carrier of T:]

[p,G] is Connection of T, InclPoset (Ids T)

{p,G} is non empty finite set

{p} is non empty trivial finite V35() V38(1) set

{{p,G},{p}} is non empty finite V35() set

rng p is finite Element of bool the carrier of (InclPoset (Ids T))

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

dom p is finite Element of bool the carrier of T

TT is set

xp is set

G . TT is set

p . xp is set

f is Element of the carrier of (InclPoset (Ids T))

G . f is Element of the carrier of T

H is non empty finite directed lower Element of bool the carrier of T

sup H is Element of the carrier of T

p . (sup H) is Element of the carrier of (InclPoset (Ids T))

downarrow (sup H) is non empty finite directed lower Element of bool the carrier of T

{(sup H)} is non empty trivial finite V38(1) Element of bool the carrier of T

downarrow {(sup H)} is non empty finite lower Element of bool the carrier of T

f is Element of the carrier of T

p . f is Element of the carrier of (InclPoset (Ids T))

H is non empty finite directed lower Element of bool the carrier of T

sup H is Element of the carrier of T

downarrow f is non empty finite directed lower Element of bool the carrier of T

{f} is non empty trivial finite V38(1) Element of bool the carrier of T

downarrow {f} is non empty finite lower Element of bool the carrier of T

sup (downarrow f) is Element of the carrier of T

dom G is Element of bool the carrier of (InclPoset (Ids T))

G is V7() V10( the carrier of (InclPoset (Ids T))) V11( the carrier of T) Function-like quasi_total Element of bool [: the carrier of (InclPoset (Ids T)), the carrier of T:]

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

the carrier of T is non empty set

bool the carrier of T is non empty set

x is Element of the carrier of T

x "/\" is V7() V10( the carrier of T) V11( the carrier of T) Function-like quasi_total monotone Element of bool [: the carrier of T, the carrier of T:]

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

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

p is non empty Element of bool the carrier of T

(x "/\") .: p is Element of bool the carrier of T

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

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

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

G is set

xp is Element of the carrier of T

{ (x "/\" b

TT is Element of the carrier of T

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

f is Element of the carrier of T

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

xp "/\" xp is Element of the carrier of T

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

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

the carrier of T is non empty set

x is Element of the carrier of T

x "/\" is V7() V10( the carrier of T) V11( the carrier of T) Function-like quasi_total monotone Element of bool [: the carrier of T, the carrier of T:]

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

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

p is Element of the carrier of T

G is Element of the carrier of T

{p,G} is non empty finite Element of bool the carrier of T

bool the carrier of T is non empty set

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

the carrier of T is non empty set

x is Element of the carrier of T

x "/\" is V7() V10( the carrier of T) V11( the carrier of T) Function-like quasi_total monotone Element of bool [: the carrier of T, the carrier of T:]

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

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

T is non empty TopSpace-like anti-discrete almost_discrete extremally_disconnected hereditarily_extremally_disconnected TopStruct

the carrier of T is non empty set

{ the carrier of T} is non empty trivial finite V38(1) set

bool the carrier of T is non empty set

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

x is Element of the carrier of T

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

G is set

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

TT 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

Intersect G is Element of bool the carrier of T

meet G is Element of bool the carrier of T

TT is Element of bool the carrier of T

T is non empty TopSpace-like anti-discrete almost_discrete extremally_disconnected hereditarily_extremally_disconnected 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

{ the carrier of T} is non empty trivial finite V38(1) set

x is Element of the carrier of T

p is non empty x -quasi_basis open Element of bool (bool the carrier of T)

G is set

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

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

x is non empty quasi_basis open Element of bool (bool the carrier of T)

p is Element of the carrier of T

{ b

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

TT is set

xp is Element of bool the carrier of T

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

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

f is Element of bool the carrier of T

H is Element of bool the carrier of T

f is set

H is Element of bool the carrier of T

Intersect xp is Element of bool the carrier of T

f is Element of bool the carrier of T

H is Element of bool the carrier of T

T is non empty 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 Element of bool the carrier of T

Cl x is Element of bool the carrier of T

p is Element of the carrier of T

G is p -quasi_basis open Element of bool (bool the carrier of T)

TT is Element of bool the carrier of T

x /\ TT is Element of bool the carrier of T

T is non empty 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 Element of bool the carrier of T

p is Element of the carrier of T

the p -quasi_basis open Element of bool (bool the carrier of T) is p -quasi_basis open Element of bool (bool the carrier of T)

TT is Element of bool the carrier of T

T is non empty 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 Element of bool the carrier of T

Cl x is Element of bool the carrier of T

p is Element of the carrier of T

G is p -quasi_basis open Element of bool (bool the carrier of T)

TT is Element of bool the carrier of T

TT ` is Element of bool the carrier of T

the carrier of T \ TT is set

xp is Element of bool the carrier of T

T is non empty 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 Element of bool the carrier of T

Cl x is Element of bool the carrier of T

p is Element of the carrier of T

TT is Element of bool the carrier of T

G is p -quasi_basis open Element of bool (bool the carrier of T)

G is p -quasi_basis open Element of bool (bool the carrier of T)

T is non empty 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 Element of bool the carrier of T

Cl x is Element of bool the carrier of T

p is Element of the carrier of T

TT is Element of bool the carrier of T

G is p -quasi_basis open Element of bool (bool the carrier of T)

G is p -quasi_basis open Element of bool (bool the carrier of T)

T is TopStruct

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

x is Element of the carrier of T

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

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

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

TT is Element of bool the carrier of T

Int TT is Element of bool the carrier of T

Int (Int TT) 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 set

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

x is Element of the carrier of T

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

G is a_neighborhood of x

Int G is open Element of bool the carrier of T

TT is Element of bool the carrier of T

Int TT is open Element of bool the carrier of T

xp is a_neighborhood of x

f is a_neighborhood of x

G is Element of bool the carrier of T

Int G is open Element of bool the carrier of T

TT is a_neighborhood of x

Int TT is open Element of bool the carrier of T

T is TopStruct

the carrier of T is set

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

x is Element of the carrier of T

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

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

TT is Element of bool the carrier of T

Int TT is Element of bool the carrier of T

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

T is non empty TopSpace-like TopStruct

the carrier of T is non empty set

x is Element of the carrier of T

p is (T,x)

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

bool the carrier of T is non empty set

Int ([#] T) is open Element of bool the carrier of T

G is Element of bool the carrier of T

Int G is open Element of bool the carrier of T

T is non empty TopSpace-like TopStruct

the carrier of T is non empty set

x is Element of the carrier of T

p is (T,x)

T is TopStruct

the carrier of T is set

x is Element of the carrier of T

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

T is TopStruct

the carrier of T is set

x is Element of the carrier of T

T is TopStruct

the carrier of T is set

p is set

bool the carrier of T is non empty set

x is Element of the carrier of T

{ b

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

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

G is set

TT is Element of bool the carrier of T

Int TT is Element of bool the carrier of T

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

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

xp is Element of bool the carrier of T

Int xp is Element of bool the carrier of T

f is Element of bool the carrier of T

Int f is Element of bool the carrier of T

T is TopStruct

the carrier of T is set

x is Element of the carrier of T

p is (T,x)

bool the carrier of T is non empty set

{ b

G is Element of bool the carrier of T

Int G is Element of bool the carrier of T

TT is Element of bool the carrier of T

Int TT is Element of bool the carrier of T

T is TopStruct

the carrier of T is set

x is Element of the carrier of T

bool the carrier of T is non empty set

{ b

p is (T,x)

T is TopStruct

the carrier of T is set

bool the carrier of T is non empty set

x is Element of the carrier of T

{ b

T is non empty TopSpace-like TopStruct

the carrier of T is non empty set

x is Element of the carrier of T

bool the carrier of T is non empty set

{ b

p is non empty (T,x) (T,x)

T is non empty TopSpace-like anti-discrete almost_discrete extremally_disconnected hereditarily_extremally_disconnected TopStruct

the carrier of T is non empty set

{ the carrier of T} is non empty trivial finite V38(1) set

x is Element of the carrier of T

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

G is set

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

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

xp is a_neighborhood of x

Int xp is open Element of bool the carrier of T

xp is non empty (T,x)

f is Element of bool the carrier of T

Int f is open 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

T is non empty TopSpace-like anti-discrete almost_discrete extremally_disconnected hereditarily_extremally_disconnected TopStruct

the carrier of T is non empty set

{ the carrier of T} is non empty trivial finite V38(1) set

x is Element of the carrier of T

p is non empty (T,x) (T,x)

G is set

bool the carrier of T is non empty set

TT is Element of bool the carrier of T

Int TT is open 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 set

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

x is Element of the carrier of T

p is non empty x -quasi_basis open Element of bool (bool the carrier of T)

G is Element of bool the carrier of T

Int G is open Element of bool the carrier of T

TT is Element of bool the carrier of T

xp is Element of bool the carrier of T

Int xp is open Element of bool the carrier of T

T is TopStruct

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

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

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

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

G is Element of the carrier of T

T is TopStruct

the carrier of T is set

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

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

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

G is Element of the carrier of T

T is non empty TopSpace-like TopStruct

x is (T)

the carrier of T is non empty set

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

G is non empty (T, the Element of the carrier of T)

T is non empty TopSpace-like TopStruct

x is (T)

T is TopStruct

the carrier of T is set

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

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 non empty (T)

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

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

p is set

G is Element of bool the carrier of T

{ b

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

xp is set

f is Element of bool the carrier of T

Int f is open Element of bool the carrier of T

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

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

union f is Element of bool the carrier of T

H is set

A is Element of bool the carrier of T

Int A is open Element of bool the carrier of T

H is set

A is Element of the carrier of T

Int G is open Element of bool the carrier of T

Z is non empty (T,A)

X1 is Element of bool the carrier of T

Int X1 is open Element of bool the carrier of T

Int (Int X1) is open Element of bool the carrier of T

H is set

A is set

Z is Element of bool the carrier of T

Int Z is open Element of bool the carrier of T

X1 is Element of bool the carrier of T

Y1 is Element of bool the carrier of T

Int Y1 is open Element of bool the carrier of T

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

union TT is Element of bool the carrier of T

T is TopSpace-like TopStruct

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

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

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

p is Element of the carrier of T

G is Element of bool the carrier of T

Int G is open Element of bool the carrier of T

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

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

union TT is Element of bool the carrier of T

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

f is set

H is Element of bool the carrier of T

Int H is open Element of bool the carrier of T

union xp is Element of bool the carrier of T

T is non empty trivial finite 1 -element TopSpace-like T_0 T_1 T_2 regular normal T_3 T_4 discrete anti-discrete almost_discrete extremally_disconnected hereditarily_extremally_disconnected compact TopRelStr

x is non empty trivial finite 1 -element TopSpace-like T_0 T_1 T_2 regular normal T_3 T_4 reflexive transitive antisymmetric with_suprema with_infima complete discrete anti-discrete almost_discrete extremally_disconnected hereditarily_extremally_disconnected lower-bounded upper-bounded V192() connected up-complete /\-complete compact TopRelStr

the carrier of x is non empty trivial finite V38(1) set

p is Element of the carrier of x

{p} is non empty trivial finite V38(1) closed directed filtered compact Element of bool the carrier of x

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

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

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

the carrier of T is non empty trivial finite V38(1) set

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

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

[:T,T:] is strict RelStr

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

G is V7() V10( the carrier of [:T,T:]) V11( the carrier of T) Function-like quasi_total Element of bool [: the carrier of [:T,T:], the carrier of T:]

inf_op T is V7() V10( the carrier of [:T,T:]) V11( the carrier of T) Function-like quasi_total Element of bool [: the carrier of [:T,T:], the carrier of T:]

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

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

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

TT is trivial finite closed Element of bool the carrier of T

G " TT is Element of bool the carrier of [:T,T:]

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

{} [:T,T:] is empty proper V7() non-empty empty-yielding V24() V25() V26() V28() V29() V30() finite finite-yielding V35() V36() V38( {} ) open closed boundary nowhere_dense Element of bool the carrier of [:T,T:]

dom G is Element of bool the carrier of [:T,T:]

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

[: the carrier of T, the carrier of T:] is non empty V7() finite set

G " TT is Element of bool the carrier of [:T,T:]

[:{p},{p}:] is non empty V7() finite filtered Element of bool the carrier of [:x,x:]

[:x,x:] is strict RelStr

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

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

xp is set

xp is set

[p,p] is Element of the carrier of [:x,x:]

{p,p} is non empty finite set

{p} is non empty trivial finite V38(1) set

{{p,p},{p}} is non empty finite V35() set

{[p,p]} is non empty trivial V7() finite V38(1) set

G . (p,p) is set

[p,p] is set

G . [p,p] is set

p "/\" p is Element of the carrier of x

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

T is non empty TopSpace-like () TopRelStr

the carrier of T is non empty set

x is Element of the carrier of T

x "/\" is V7() V10( the carrier of T) V11( the carrier of T) Function-like quasi_total Element of bool [: the carrier of T, the carrier of T:]

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

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

p is Element of the carrier of T

(x "/\") . p is Element of the carrier of T

G is a_neighborhood of (x "/\") . p

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

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

[x,p] is Element of the carrier of [:T,T:]

[:T,T:] is strict RelStr

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

{x,p} is non empty finite set

{x} is non empty trivial finite V38(1) set

{{x,p},{x}} is non empty finite V35() set

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

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

inf_op T is V7() V10( the carrier of [:T,T:]) V11( the carrier of T) Function-like quasi_total Element of bool [: the carrier of [:T,T:], the carrier of T:]

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

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

f is V7() V10( the carrier of [:T,T:]) V11( the carrier of T) Function-like quasi_total Element of bool [: the carrier of [:T,T:], the carrier of T:]

xp is Element of the carrier of [:T,T:]

f . xp is Element of the carrier of T

f . (x,p) is set

[x,p] is set

f . [x,p] is set

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

H is a_neighborhood of xp

f .: H is Element of bool the carrier of T

bool the carrier of T is non empty set

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

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

Int H is open Element of bool the carrier of [:T,T:]

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

union A is Element of bool the carrier of [:T,T:]

Z is set

X1 is Element of bool the carrier of T

Y1 is Element of bool the carrier of T

[:X1,Y1:] is V7() Element of bool the carrier of [:T,T:]

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

Y1 is a_neighborhood of p

(x "/\") .: Y1 is Element of bool the carrier of T

b is set

dom (x "/\") is Element of bool the carrier of T

a is set

(x "/\") . a is set

a is Element of the carrier of T

[x,a] is Element of the carrier of [:T,T:]

{x,a} is non empty finite set

{{x,a},{x}} is non empty finite V35() set

dom f is Element of bool the carrier of [:T,T:]

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

f . (x,a) is set

[x,a] is set

f . [x,a] is set

T is non empty TopSpace-like () TopRelStr

the carrier of T is non empty set

x is Element of the carrier of T

x "/\" is V7() V10( the carrier of T) V11( the carrier of T) Function-like quasi_total Element of bool [: the carrier of T, the carrier of T:]

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

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