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

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

the carrier of T is set

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

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

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

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

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

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

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 .: () is Element of bool the carrier of x
downarrow (p .: ()) is Element of bool the carrier of x

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

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 .: () is Element of bool the carrier of x
downarrow (p .: ()) 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

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
{ b1 where b1 is non empty directed lower Element of bool the carrier of T : verum } is set

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
() . p is Element of the carrier of (InclPoset (Ids T))
G is Element of the carrier of 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

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
{ b1 where b1 is non empty directed lower Element of bool the carrier of T : verum } is set

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

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
{ b1 where b1 is non empty directed lower Element of bool the carrier of T : verum } is set

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))
() . p is Element of the carrier of T
G is Element of the carrier of (InclPoset (Ids 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

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
{ b1 where b1 is non empty directed lower Element of bool the carrier of T : verum } is set

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

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
{ b1 where b1 is non empty directed lower Element of bool the carrier of T : verum } is set

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 () 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:]

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 "/\" b1) where b1 is Element of the carrier of T : b1 in p } is set
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

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

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

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

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
{ b1 where b1 is Element of bool the carrier of T : ( b1 in x & p in b1 ) } is set
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
{ b1 where b1 is Element of bool the carrier of T : x in Int b1 } is set
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
{ b1 where b1 is Element of bool the carrier of T : x in Int b1 } is set
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
{ b1 where b1 is Element of bool the carrier of T : x in Int b1 } is set
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
{ b1 where b1 is Element of bool the carrier of T : x in Int b1 } is set
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
{ b1 where b1 is Element of bool the carrier of T : x in Int b1 } is set
p is non empty (T,x) (T,x)

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

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
{ b1 where b1 is Element of bool the carrier of T : ( b1 in Int x & Int b1 c= p ) } is set
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

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

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

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