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