:: YELLOW_9 semantic presentation

K259() is set
K263() is non empty non trivial V35() V36() V37() non finite V47() V48() Element of bool K259()
bool K259() is non empty set
K103() is non empty non trivial V35() V36() V37() non finite V47() V48() set
bool K103() is non empty non trivial non finite set
I[01] is non empty strict TopSpace-like TopStruct
the carrier of I[01] is non empty set
{} is empty Relation-like non-empty empty-yielding Function-like one-to-one constant functional V35() V36() V37() V39() V40() V41() finite finite-yielding V46() V47() V49( {} ) set
the empty Relation-like non-empty empty-yielding Function-like one-to-one constant functional V35() V36() V37() V39() V40() V41() finite finite-yielding V46() V47() V49( {} ) set is empty Relation-like non-empty empty-yielding Function-like one-to-one constant functional V35() V36() V37() V39() V40() V41() finite finite-yielding V46() V47() V49( {} ) set
1 is non empty V35() V36() V37() V41() finite V47() Element of K263()
{{},1} is non empty finite V46() set
bool K263() is non empty non trivial non finite set
bool {} is non empty finite V46() set
{{}} is non empty trivial functional finite V46() V49(1) set
union {} is V35() V36() V37() V41() finite V47() set
F₁() is non empty set
bool F₁() is non empty set
F₃() is Element of bool F₁()
F₂() is Element of bool F₁()
{ F₄(b₁) where b₁ is Element of F₁() : b₁ in F₂() } is set
{ F₄(b₁) where b₁ is Element of F₁() : b₁ in F₃() } is set
L is set
T1 is Element of F₁()
F₄(T1) is Element of F₁()
F₄(F₄(T1)) is Element of F₁()
L is set
T1 is Element of F₁()
F₄(T1) is Element of F₁()
T2 is Element of F₁()
F₄(T2) is Element of F₁()
F₁() is non empty RelStr
the carrier of F₁() is non empty set
bool the carrier of F₁() is non empty set
bool (bool the carrier of F₁()) is non empty set
F₂() is Element of bool (bool the carrier of F₁())
F₃() is set
{ F₄(b₁) where b₁ is Element of the carrier of F₁() : b₁ in F₃() } is set
COMPLEMENT F₂() is Element of bool (bool the carrier of F₁())
{ (F₄(b₁) `) where b<sub>1</sub> is Element of the carrier of F<sub>1</sub>() : b<sub>1</sub> in F<sub>3</sub>() } is set
L is set
T1 is Element of bool the carrier of F<sub>1</sub>()
T1 ` is Element of bool the carrier of F₁()
(T1 `) ` is Element of bool the carrier of F₁()
T2 is Element of the carrier of F₁()
F₄(T2) is Element of bool the carrier of F₁()
L is set
T1 is Element of the carrier of F₁()
F₄(T1) is Element of bool the carrier of F₁()
F₄(T1) ` is Element of bool the carrier of F<sub>1</sub>()
F<sub>1</sub>() is non empty RelStr
the carrier of F<sub>1</sub>() is non empty set
bool the carrier of F<sub>1</sub>() is non empty set
bool (bool the carrier of F<sub>1</sub>()) is non empty set
F<sub>2</sub>() is Element of bool (bool the carrier of F<sub>1</sub>())
F<sub>3</sub>() is set
{ (F<sub>4</sub>(b<sub>1</sub>) `) where b₁ is Element of the carrier of F₁() : b₁ in F₃() } is set
COMPLEMENT F₂() is Element of bool (bool the carrier of F₁())
{ F₄(b₁) where b₁ is Element of the carrier of F₁() : b₁ in F₃() } is set
L is set
T1 is Element of bool the carrier of F₁()
T1 ` is Element of bool the carrier of F<sub>1</sub>()
(T1 `) ` is Element of bool the carrier of F<sub>1</sub>()
T2 is Element of the carrier of F<sub>1</sub>()
F<sub>4</sub>(T2) is Element of bool the carrier of F<sub>1</sub>()
F<sub>4</sub>(T2) ` is Element of bool the carrier of F₁()
L is set
T1 is Element of the carrier of F₁()
F₄(T1) is Element of bool the carrier of F₁()
F₄(T1) ` is Element of bool the carrier of F<sub>1</sub>()
L is non empty RelStr
the carrier of L is non empty set
T2 is Element of the carrier of L
T1 is Element of the carrier of L
uparrow T1 is Element of bool the carrier of L
bool the carrier of L is non empty set
{T1} is non empty trivial finite V49(1) Element of bool the carrier of L
uparrow {T1} is Element of bool the carrier of L
(uparrow T1) ` is Element of bool the carrier of L
the carrier of L \ (uparrow T1) is Element of bool the carrier of L
F₃() is Relation-like Function-like set
F₁() is TopSpace-like TopStruct
the carrier of F₁() is set
bool the carrier of F₁() is non empty set
{ F₂(b₁) where b₁ is Element of bool the carrier of F₁() : P₁[b₁] } is set
union { F₂(b₁) where b₁ is Element of bool the carrier of F₁() : P₁[b₁] } is set
F₃() " (union { F₂(b₁) where b₁ is Element of bool the carrier of F₁() : P₁[b₁] } ) is set
{ (F₃() " F₂(b₁)) where b₁ is Element of bool the carrier of F₁() : P₁[b₁] } is set
union { (F₃() " F₂(b₁)) where b₁ is Element of bool the carrier of F₁() : P₁[b₁] } is set
T2 is set
dom F₃() is set
F₃() . T2 is set
B1 is set
B2 is Element of bool the carrier of F₁()
F₂(B2) is set
F₃() " F₂(B2) is set
T2 is set
B1 is set
B2 is Element of bool the carrier of F₁()
F₂(B2) is set
F₃() " F₂(B2) is set
F₃() . T2 is set
L is 1-sorted
the carrier of L is set
T1 is non empty 1-sorted
the carrier of T1 is non empty set
[: the carrier of L, the carrier of T1:] is Relation-like set
bool [: the carrier of L, the carrier of T1:] is non empty set
bool the carrier of T1 is non empty set
T2 is Relation-like the carrier of L -defined the carrier of T1 -valued Function-like V27( the carrier of L) quasi_total Element of bool [: the carrier of L, the carrier of T1:]
B1 is Element of bool the carrier of T1
T2 " B1 is Element of bool the carrier of L
bool the carrier of L is non empty set
(T2 " B1) ` is Element of bool the carrier of L
B1 ` is Element of bool the carrier of T1
T2 " (B1 `) is Element of bool the carrier of L
the carrier of L \ (T2 " B1) is Element of bool the carrier of L
T2 " the carrier of T1 is Element of bool the carrier of L
(T2 " the carrier of T1) \ (T2 " B1) is Element of bool the carrier of L
the carrier of T1 \ B1 is Element of bool the carrier of T1
T2 " ( the carrier of T1 \ B1) is Element of bool the carrier of L
L is 1-sorted
the carrier of L is set
bool the carrier of L is non empty set
bool (bool the carrier of L) is non empty set
T1 is Element of bool (bool the carrier of L)
COMPLEMENT T1 is Element of bool (bool the carrier of L)
{ (b<sub>1</sub> `) where b₁ is Element of bool the carrier of L : b₁ in T1 } is set
B1 is set
B2 is Element of bool the carrier of L
B2 ` is Element of bool the carrier of L
(B2 `) ` is Element of bool the carrier of L
B1 is set
B2 is Element of bool the carrier of L
B2 ` is Element of bool the carrier of L
L is non empty RelStr
the carrier of L is non empty set
bool the carrier of L is non empty set
T1 is Element of bool the carrier of L
uparrow T1 is Element of bool the carrier of L
{ (uparrow b₁) where b₁ is Element of the carrier of L : b₁ in T1 } is set
union { (uparrow b₁) where b₁ is Element of the carrier of L : b₁ in T1 } is set
downarrow T1 is Element of bool the carrier of L
{ (downarrow b₁) where b₁ is Element of the carrier of L : b₁ in T1 } is set
union { (downarrow b₁) where b₁ is Element of the carrier of L : b₁ in T1 } is set
{ b₁ where b₁ is Element of the carrier of L : ex b₂ being Element of the carrier of L st
( b₂ <= b₁ & b₂ in T1 ) } is set
{ b₁ where b₁ is Element of the carrier of L : ex b₂ being Element of the carrier of L st
( b₁ <= b₂ & b₂ in T1 ) } is set
T2 is set
B1 is Element of the carrier of L
B2 is Element of the carrier of L
B2 is Element of the carrier of L
uparrow B2 is Element of bool the carrier of L
{B2} is non empty trivial finite V49(1) Element of bool the carrier of L
uparrow {B2} is Element of bool the carrier of L
T2 is set
B1 is set
B2 is Element of the carrier of L
uparrow B2 is Element of bool the carrier of L
{B2} is non empty trivial finite V49(1) Element of bool the carrier of L
uparrow {B2} is Element of bool the carrier of L
B1 is Element of the carrier of L
T2 is set
B1 is Element of the carrier of L
B2 is Element of the carrier of L
B2 is Element of the carrier of L
downarrow B2 is Element of bool the carrier of L
{B2} is non empty trivial finite V49(1) Element of bool the carrier of L
downarrow {B2} is Element of bool the carrier of L
T2 is set
B1 is set
B2 is Element of the carrier of L
downarrow B2 is Element of bool the carrier of L
{B2} is non empty trivial finite V49(1) Element of bool the carrier of L
downarrow {B2} is Element of bool the carrier of L
B1 is Element of the carrier of L
L is non empty RelStr
the carrier of L is non empty set
bool the carrier of L is non empty set
bool (bool the carrier of L) is non empty set
T1 is Element of bool (bool the carrier of L)
Intersect T1 is Element of bool the carrier of L
T2 is Element of bool the carrier of L
{ ((uparrow b₁) `) where b<sub>1</sub> is Element of the carrier of L : b<sub>1</sub> in T2 } is set
uparrow T2 is Element of bool the carrier of L
(uparrow T2) ` is Element of bool the carrier of L
{ (H₁(b₁) `) where b<sub>1</sub> is Element of the carrier of L : b<sub>1</sub> in T2 } is set
COMPLEMENT T1 is Element of bool (bool the carrier of L)
{ H<sub>1</sub>(b<sub>1</sub>) where b<sub>1</sub> is Element of the carrier of L : b<sub>1</sub> in T2 } is set
B1 is Element of bool (bool the carrier of L)
COMPLEMENT B1 is Element of bool (bool the carrier of L)
union B1 is Element of bool the carrier of L
(union B1) ` is Element of bool the carrier of L
the non empty trivial finite 1 -element TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete discrete V129() V130() V131() V132() lower-bounded upper-bounded V194() connected up-complete /\-complete strict TopRelStr is non empty trivial finite 1 -element TopSpace-like reflexive transitive antisymmetric with_suprema with_infima complete discrete V129() V130() V131() V132() lower-bounded upper-bounded V194() connected up-complete /\-complete strict TopRelStr
L is non empty RelStr
the carrier of L is non empty set
T1 is non empty reflexive antisymmetric upper-bounded RelStr
the carrier of T1 is non empty set
[: the carrier of L, the carrier of T1:] is non empty Relation-like set
bool [: the carrier of L, the carrier of T1:] is non empty set
Top T1 is Element of the carrier of T1
"/\" ({},T1) is Element of the carrier of T1
L --> (Top T1) is non empty Relation-like the carrier of L -defined the carrier of T1 -valued Function-like V27( the carrier of L) quasi_total Element of bool [: the carrier of L, the carrier of T1:]
K354( the carrier of T1, the carrier of L,(Top T1)) is non empty Relation-like the carrier of L -defined the carrier of T1 -valued Function-like V27( the carrier of L) quasi_total Element of bool [: the carrier of L, the carrier of T1:]
T2 is non empty Relation-like the carrier of L -defined the carrier of T1 -valued Function-like V27( the carrier of L) quasi_total Element of bool [: the carrier of L, the carrier of T1:]
bool the carrier of L is non empty set
B1 is Element of bool the carrier of L
T2 .: B1 is Element of bool the carrier of T1
bool the carrier of T1 is non empty set
"/\" ((T2 .: B1),T1) is Element of the carrier of T1
"/\" (B1,L) is Element of the carrier of L
T2 . ("/\" (B1,L)) is Element of the carrier of T1
rng T2 is non empty Element of bool the carrier of T1
{(Top T1)} is non empty trivial finite V49(1) Element of bool the carrier of T1
T2 . ("/\" (B1,L)) is Element of the carrier of T1
L is non empty RelStr
the carrier of L is non empty set
T1 is non empty reflexive antisymmetric lower-bounded RelStr
the carrier of T1 is non empty set
[: the carrier of L, the carrier of T1:] is non empty Relation-like set
bool [: the carrier of L, the carrier of T1:] is non empty set
Bottom T1 is Element of the carrier of T1
sup {} is Element of the carrier of T1
L --> (Bottom T1) is non empty Relation-like the carrier of L -defined the carrier of T1 -valued Function-like V27( the carrier of L) quasi_total Element of bool [: the carrier of L, the carrier of T1:]
K354( the carrier of T1, the carrier of L,(Bottom T1)) is non empty Relation-like the carrier of L -defined the carrier of T1 -valued Function-like V27( the carrier of L) quasi_total Element of bool [: the carrier of L, the carrier of T1:]
T2 is non empty Relation-like the carrier of L -defined the carrier of T1 -valued Function-like V27( the carrier of L) quasi_total Element of bool [: the carrier of L, the carrier of T1:]
bool the carrier of L is non empty set
B1 is Element of bool the carrier of L
T2 .: B1 is Element of bool the carrier of T1
bool the carrier of T1 is non empty set
sup (T2 .: B1) is Element of the carrier of T1
sup B1 is Element of the carrier of L
T2 . (sup B1) is Element of the carrier of T1
rng T2 is non empty Element of bool the carrier of T1
{(Bottom T1)} is non empty trivial finite V49(1) Element of bool the carrier of T1
T2 . (sup B1) is Element of the carrier of T1
T1 is 1-sorted
the carrier of T1 is set
L is 1-sorted
the carrier of L is set
id the carrier of T1 is Relation-like the carrier of T1 -defined the carrier of T1 -valued Function-like one-to-one V27( the carrier of T1) quasi_total Element of bool [: the carrier of T1, the carrier of T1:]
[: the carrier of T1, the carrier of T1:] is Relation-like set
bool [: the carrier of T1, the carrier of T1:] is non empty set
dom (id the carrier of T1) is Element of bool the carrier of T1
bool the carrier of T1 is non empty set
rng (id the carrier of T1) is Element of bool the carrier of T1
[: the carrier of T1, the carrier of L:] is Relation-like set
bool [: the carrier of T1, the carrier of L:] is non empty set
L is non empty RelStr
T1 is non empty SubRelStr of L
(L,T1) is non empty Relation-like the carrier of T1 -defined the carrier of L -valued Function-like V27( the carrier of T1) quasi_total Element of bool [: the carrier of T1, the carrier of L:]
the carrier of T1 is non empty set
the carrier of L is non empty set
[: the carrier of T1, the carrier of L:] is non empty Relation-like set
bool [: the carrier of T1, the carrier of L:] is non empty set
T2 is Element of the carrier of T1
B1 is Element of the carrier of T1
(L,T1) . T2 is Element of the carrier of L
(L,T1) . B1 is Element of the carrier of L
id the carrier of T1 is non empty Relation-like the carrier of T1 -defined the carrier of T1 -valued Function-like one-to-one V27( the carrier of T1) quasi_total Element of bool [: the carrier of T1, the carrier of T1:]
[: the carrier of T1, the carrier of T1:] is non empty Relation-like set
bool [: the carrier of T1, the carrier of T1:] is non empty set
(L,T1) . T2 is Element of the carrier of L
B2 is Element of the carrier of L
(L,T1) . B1 is Element of the carrier of L
B1 is Element of the carrier of L
L is non empty RelStr
the carrier of L is non empty set
bool the carrier of L is non empty set
T1 is non empty Element of bool the carrier of L
subrelstr T1 is non empty strict full SubRelStr of L
(L,(subrelstr T1)) is non empty Relation-like the carrier of (subrelstr T1) -defined the carrier of L -valued Function-like V27( the carrier of (subrelstr T1)) quasi_total monotone Element of bool [: the carrier of (subrelstr T1), the carrier of L:]
the carrier of (subrelstr T1) is non empty set
[: the carrier of (subrelstr T1), the carrier of L:] is non empty Relation-like set
bool [: the carrier of (subrelstr T1), the carrier of L:] is non empty set
(subrelstr T1) +id is non empty strict monotone eventually-directed NetStr over subrelstr T1
(L,(subrelstr T1)) * ((subrelstr T1) +id) is non empty strict NetStr over L
(subrelstr T1) opp+id is non empty strict antitone eventually-filtered NetStr over subrelstr T1
(L,(subrelstr T1)) * ((subrelstr T1) opp+id) is non empty strict NetStr over L
L is non empty RelStr
the carrier of L is non empty set
bool the carrier of L is non empty set
T1 is non empty Element of bool the carrier of L
(L,T1) is non empty strict NetStr over L
subrelstr T1 is non empty strict full SubRelStr of L
(L,(subrelstr T1)) is non empty Relation-like the carrier of (subrelstr T1) -defined the carrier of L -valued Function-like V27( the carrier of (subrelstr T1)) quasi_total monotone Element of bool [: the carrier of (subrelstr T1), the carrier of L:]
the carrier of (subrelstr T1) is non empty set
[: the carrier of (subrelstr T1), the carrier of L:] is non empty Relation-like set
bool [: the carrier of (subrelstr T1), the carrier of L:] is non empty set
(subrelstr T1) +id is non empty strict monotone eventually-directed NetStr over subrelstr T1
(L,(subrelstr T1)) * ((subrelstr T1) +id) is non empty strict NetStr over L
the carrier of (L,T1) is non empty set
the InternalRel of (L,T1) is Relation-like the carrier of (L,T1) -defined the carrier of (L,T1) -valued Element of bool [: the carrier of (L,T1), the carrier of (L,T1):]
[: the carrier of (L,T1), the carrier of (L,T1):] is non empty Relation-like set
bool [: the carrier of (L,T1), the carrier of (L,T1):] is non empty set
RelStr(# the carrier of (L,T1), the InternalRel of (L,T1) #) is strict RelStr
the carrier of ((subrelstr T1) +id) is non empty set
the InternalRel of ((subrelstr T1) +id) is Relation-like the carrier of ((subrelstr T1) +id) -defined the carrier of ((subrelstr T1) +id) -valued Element of bool [: the carrier of ((subrelstr T1) +id), the carrier of ((subrelstr T1) +id):]
[: the carrier of ((subrelstr T1) +id), the carrier of ((subrelstr T1) +id):] is non empty Relation-like set
bool [: the carrier of ((subrelstr T1) +id), the carrier of ((subrelstr T1) +id):] is non empty set
RelStr(# the carrier of ((subrelstr T1) +id), the InternalRel of ((subrelstr T1) +id) #) is strict RelStr
the mapping of (L,T1) is non empty Relation-like the carrier of (L,T1) -defined the carrier of L -valued Function-like V27( the carrier of (L,T1)) quasi_total Element of bool [: the carrier of (L,T1), the carrier of L:]
[: the carrier of (L,T1), the carrier of L:] is non empty Relation-like set
bool [: the carrier of (L,T1), the carrier of L:] is non empty set
the mapping of ((subrelstr T1) +id) is non empty Relation-like the carrier of ((subrelstr T1) +id) -defined the carrier of (subrelstr T1) -valued Function-like V27( the carrier of ((subrelstr T1) +id)) quasi_total Element of bool [: the carrier of ((subrelstr T1) +id), the carrier of (subrelstr T1):]
[: the carrier of ((subrelstr T1) +id), the carrier of (subrelstr T1):] is non empty Relation-like set
bool [: the carrier of ((subrelstr T1) +id), the carrier of (subrelstr T1):] is non empty set
(L,(subrelstr T1)) * the mapping of ((subrelstr T1) +id) is non empty Relation-like the carrier of ((subrelstr T1) +id) -defined the carrier of L -valued Function-like V27( the carrier of ((subrelstr T1) +id)) quasi_total Element of bool [: the carrier of ((subrelstr T1) +id), the carrier of L:]
[: the carrier of ((subrelstr T1) +id), the carrier of L:] is non empty Relation-like set
bool [: the carrier of ((subrelstr T1) +id), the carrier of L:] is non empty set
the InternalRel of (subrelstr T1) is Relation-like the carrier of (subrelstr T1) -defined the carrier of (subrelstr T1) -valued Element of bool [: the carrier of (subrelstr T1), the carrier of (subrelstr T1):]
[: the carrier of (subrelstr T1), the carrier of (subrelstr T1):] is non empty Relation-like set
bool [: the carrier of (subrelstr T1), the carrier of (subrelstr T1):] is non empty set
the InternalRel of L is Relation-like the carrier of L -defined the carrier of L -valued Element of bool [: the carrier of L, the carrier of L:]
[: the carrier of L, the carrier of L:] is non empty Relation-like set
bool [: the carrier of L, the carrier of L:] is non empty set
T2 is SubRelStr of L
the InternalRel of T2 is Relation-like the carrier of T2 -defined the carrier of T2 -valued Element of bool [: the carrier of T2, the carrier of T2:]
the carrier of T2 is set
[: the carrier of T2, the carrier of T2:] is Relation-like set
bool [: the carrier of T2, the carrier of T2:] is non empty set
the InternalRel of L |_2 the carrier of T2 is Relation-like set
the InternalRel of L /\ [: the carrier of T2, the carrier of T2:] is Relation-like the carrier of L -defined the carrier of L -valued set
B1 is Element of the carrier of (L,T1)
(L,T1) . B1 is Element of the carrier of L
the mapping of (L,T1) . B1 is Element of the carrier of L
id (subrelstr T1) is non empty Relation-like the carrier of (subrelstr T1) -defined the carrier of (subrelstr T1) -valued Function-like V27( the carrier of (subrelstr T1)) quasi_total monotone Element of bool [: the carrier of (subrelstr T1), the carrier of (subrelstr T1):]
id the carrier of (subrelstr T1) is non empty Relation-like the carrier of (subrelstr T1) -defined the carrier of (subrelstr T1) -valued Function-like one-to-one V27( the carrier of (subrelstr T1)) quasi_total Element of bool [: the carrier of (subrelstr T1), the carrier of (subrelstr T1):]
id T1 is non empty Relation-like T1 -defined T1 -valued Function-like one-to-one V27(T1) quasi_total Element of bool [:T1,T1:]
[:T1,T1:] is non empty Relation-like set
bool [:T1,T1:] is non empty set
dom (id T1) is non empty Element of bool T1
bool T1 is non empty set
L is non empty RelStr
the carrier of L is non empty set
bool the carrier of L is non empty set
L ~ is non empty strict RelStr
T1 is non empty Element of bool the carrier of L
(L,T1) is non empty strict NetStr over L
subrelstr T1 is non empty strict full SubRelStr of L
(L,(subrelstr T1)) is non empty Relation-like the carrier of (subrelstr T1) -defined the carrier of L -valued Function-like V27( the carrier of (subrelstr T1)) quasi_total monotone Element of bool [: the carrier of (subrelstr T1), the carrier of L:]
the carrier of (subrelstr T1) is non empty set
[: the carrier of (subrelstr T1), the carrier of L:] is non empty Relation-like set
bool [: the carrier of (subrelstr T1), the carrier of L:] is non empty set
(subrelstr T1) opp+id is non empty strict antitone eventually-filtered NetStr over subrelstr T1
(L,(subrelstr T1)) * ((subrelstr T1) opp+id) is non empty strict NetStr over L
the carrier of (L,T1) is non empty set
the InternalRel of (L,T1) is Relation-like the carrier of (L,T1) -defined the carrier of (L,T1) -valued Element of bool [: the carrier of (L,T1), the carrier of (L,T1):]
[: the carrier of (L,T1), the carrier of (L,T1):] is non empty Relation-like set
bool [: the carrier of (L,T1), the carrier of (L,T1):] is non empty set
RelStr(# the carrier of (L,T1), the InternalRel of (L,T1) #) is strict RelStr
the carrier of ((subrelstr T1) opp+id) is non empty set
the InternalRel of ((subrelstr T1) opp+id) is Relation-like the carrier of ((subrelstr T1) opp+id) -defined the carrier of ((subrelstr T1) opp+id) -valued Element of bool [: the carrier of ((subrelstr T1) opp+id), the carrier of ((subrelstr T1) opp+id):]
[: the carrier of ((subrelstr T1) opp+id), the carrier of ((subrelstr T1) opp+id):] is non empty Relation-like set
bool [: the carrier of ((subrelstr T1) opp+id), the carrier of ((subrelstr T1) opp+id):] is non empty set
RelStr(# the carrier of ((subrelstr T1) opp+id), the InternalRel of ((subrelstr T1) opp+id) #) is strict RelStr
the mapping of (L,T1) is non empty Relation-like the carrier of (L,T1) -defined the carrier of L -valued Function-like V27( the carrier of (L,T1)) quasi_total Element of bool [: the carrier of (L,T1), the carrier of L:]
[: the carrier of (L,T1), the carrier of L:] is non empty Relation-like set
bool [: the carrier of (L,T1), the carrier of L:] is non empty set
the mapping of ((subrelstr T1) opp+id) is non empty Relation-like the carrier of ((subrelstr T1) opp+id) -defined the carrier of (subrelstr T1) -valued Function-like V27( the carrier of ((subrelstr T1) opp+id)) quasi_total Element of bool [: the carrier of ((subrelstr T1) opp+id), the carrier of (subrelstr T1):]
[: the carrier of ((subrelstr T1) opp+id), the carrier of (subrelstr T1):] is non empty Relation-like set
bool [: the carrier of ((subrelstr T1) opp+id), the carrier of (subrelstr T1):] is non empty set
(L,(subrelstr T1)) * the mapping of ((subrelstr T1) opp+id) is non empty Relation-like the carrier of ((subrelstr T1) opp+id) -defined the carrier of L -valued Function-like V27( the carrier of ((subrelstr T1) opp+id)) quasi_total Element of bool [: the carrier of ((subrelstr T1) opp+id), the carrier of L:]
[: the carrier of ((subrelstr T1) opp+id), the carrier of L:] is non empty Relation-like set
bool [: the carrier of ((subrelstr T1) opp+id), the carrier of L:] is non empty set
the InternalRel of (subrelstr T1) is Relation-like the carrier of (subrelstr T1) -defined the carrier of (subrelstr T1) -valued Element of bool [: the carrier of (subrelstr T1), the carrier of (subrelstr T1):]
[: the carrier of (subrelstr T1), the carrier of (subrelstr T1):] is non empty Relation-like set
bool [: the carrier of (subrelstr T1), the carrier of (subrelstr T1):] is non empty set
the InternalRel of (subrelstr T1) ~ is Relation-like the carrier of (subrelstr T1) -defined the carrier of (subrelstr T1) -valued Element of bool [: the carrier of (subrelstr T1), the carrier of (subrelstr T1):]
the InternalRel of L is Relation-like the carrier of L -defined the carrier of L -valued Element of bool [: the carrier of L, the carrier of L:]
[: the carrier of L, the carrier of L:] is non empty Relation-like set
bool [: the carrier of L, the carrier of L:] is non empty set
the InternalRel of L ~ is Relation-like the carrier of L -defined the carrier of L -valued Element of bool [: the carrier of L, the carrier of L:]
RelStr(# the carrier of L,( the InternalRel of L ~) #) is strict RelStr
the InternalRel of L |_2 T1 is Relation-like set
[:T1,T1:] is non empty Relation-like set
the InternalRel of L /\ [:T1,T1:] is Relation-like the carrier of L -defined the carrier of L -valued set
( the InternalRel of L ~) |_2 T1 is Relation-like set
( the InternalRel of L ~) /\ [:T1,T1:] is Relation-like the carrier of L -defined the carrier of L -valued set
the InternalRel of (L ~) is Relation-like the carrier of (L ~) -defined the carrier of (L ~) -valued Element of bool [: the carrier of (L ~), the carrier of (L ~):]
the carrier of (L ~) is non empty set
[: the carrier of (L ~), the carrier of (L ~):] is non empty Relation-like set
bool [: the carrier of (L ~), the carrier of (L ~):] is non empty set
T2 is SubRelStr of L ~
the InternalRel of T2 is Relation-like the carrier of T2 -defined the carrier of T2 -valued Element of bool [: the carrier of T2, the carrier of T2:]
the carrier of T2 is set
[: the carrier of T2, the carrier of T2:] is Relation-like set
bool [: the carrier of T2, the carrier of T2:] is non empty set
the InternalRel of (L ~) |_2 the carrier of T2 is Relation-like set
the InternalRel of (L ~) /\ [: the carrier of T2, the carrier of T2:] is Relation-like the carrier of (L ~) -defined the carrier of (L ~) -valued set
B1 is Element of the carrier of (L,T1)
(L,T1) . B1 is Element of the carrier of L
the mapping of (L,T1) . B1 is Element of the carrier of L
id (subrelstr T1) is non empty Relation-like the carrier of (subrelstr T1) -defined the carrier of (subrelstr T1) -valued Function-like V27( the carrier of (subrelstr T1)) quasi_total monotone Element of bool [: the carrier of (subrelstr T1), the carrier of (subrelstr T1):]
id the carrier of (subrelstr T1) is non empty Relation-like the carrier of (subrelstr T1) -defined the carrier of (subrelstr T1) -valued Function-like one-to-one V27( the carrier of (subrelstr T1)) quasi_total Element of bool [: the carrier of (subrelstr T1), the carrier of (subrelstr T1):]
id T1 is non empty Relation-like T1 -defined T1 -valued Function-like one-to-one V27(T1) quasi_total Element of bool [:T1,T1:]
bool [:T1,T1:] is non empty set
dom (id T1) is non empty Element of bool T1
bool T1 is non empty set
L is non empty reflexive RelStr
the carrier of L is non empty set
bool the carrier of L is non empty set
T1 is non empty Element of bool the carrier of L
(L,T1) is non empty strict NetStr over L
subrelstr T1 is non empty strict reflexive full SubRelStr of L
(L,(subrelstr T1)) is non empty Relation-like the carrier of (subrelstr T1) -defined the carrier of L -valued Function-like V27( the carrier of (subrelstr T1)) quasi_total monotone Element of bool [: the carrier of (subrelstr T1), the carrier of L:]
the carrier of (subrelstr T1) is non empty set
[: the carrier of (subrelstr T1), the carrier of L:] is non empty Relation-like set
bool [: the carrier of (subrelstr T1), the carrier of L:] is non empty set
(subrelstr T1) +id is non empty reflexive strict monotone eventually-directed NetStr over subrelstr T1
(L,(subrelstr T1)) * ((subrelstr T1) +id) is non empty reflexive strict NetStr over L
(L,T1) is non empty strict NetStr over L
(subrelstr T1) opp+id is non empty reflexive strict antitone eventually-filtered NetStr over subrelstr T1
(L,(subrelstr T1)) * ((subrelstr T1) opp+id) is non empty reflexive strict NetStr over L
L is non empty transitive RelStr
the carrier of L is non empty set
bool the carrier of L is non empty set
T1 is non empty Element of bool the carrier of L
(L,T1) is non empty strict NetStr over L
subrelstr T1 is non empty strict transitive full SubRelStr of L
(L,(subrelstr T1)) is non empty Relation-like the carrier of (subrelstr T1) -defined the carrier of L -valued Function-like V27( the carrier of (subrelstr T1)) quasi_total monotone Element of bool [: the carrier of (subrelstr T1), the carrier of L:]
the carrier of (subrelstr T1) is non empty set
[: the carrier of (subrelstr T1), the carrier of L:] is non empty Relation-like set
bool [: the carrier of (subrelstr T1), the carrier of L:] is non empty set
(subrelstr T1) +id is non empty transitive strict monotone eventually-directed NetStr over subrelstr T1
(L,(subrelstr T1)) * ((subrelstr T1) +id) is non empty transitive strict NetStr over L
(L,T1) is non empty strict NetStr over L
(subrelstr T1) opp+id is non empty transitive strict antitone eventually-filtered NetStr over subrelstr T1
(L,(subrelstr T1)) * ((subrelstr T1) opp+id) is non empty transitive strict NetStr over L
L is non empty reflexive RelStr
the carrier of L is non empty set
bool the carrier of L is non empty set
T1 is directed Element of bool the carrier of L
subrelstr T1 is strict reflexive full SubRelStr of L
the carrier of (subrelstr T1) is set
T2 is Element of the carrier of (subrelstr T1)
[#] (subrelstr T1) is non proper Element of bool the carrier of (subrelstr T1)
bool the carrier of (subrelstr T1) is non empty set
B1 is Element of the carrier of (subrelstr T1)
B2 is Element of the carrier of L
B1 is Element of the carrier of L
B2 is Element of the carrier of L
a is Element of the carrier of (subrelstr T1)
L is non empty reflexive RelStr
the carrier of L is non empty set
bool the carrier of L is non empty set
T1 is non empty directed Element of bool the carrier of L
(L,T1) is non empty reflexive strict NetStr over L
subrelstr T1 is non empty strict reflexive full directed SubRelStr of L
(L,(subrelstr T1)) is non empty Relation-like the carrier of (subrelstr T1) -defined the carrier of L -valued Function-like V27( the carrier of (subrelstr T1)) quasi_total monotone Element of bool [: the carrier of (subrelstr T1), the carrier of L:]
the carrier of (subrelstr T1) is non empty set
[: the carrier of (subrelstr T1), the carrier of L:] is non empty Relation-like set
bool [: the carrier of (subrelstr T1), the carrier of L:] is non empty set
(subrelstr T1) +id is non empty reflexive strict directed monotone eventually-directed NetStr over subrelstr T1
(L,(subrelstr T1)) * ((subrelstr T1) +id) is non empty reflexive strict directed NetStr over L
L is non empty reflexive RelStr
the carrier of L is non empty set
bool the carrier of L is non empty set
T1 is non empty filtered Element of bool the carrier of L
subrelstr T1 is non empty strict reflexive full SubRelStr of L
(subrelstr T1) opp+id is non empty reflexive strict antitone eventually-filtered NetStr over subrelstr T1
the carrier of ((subrelstr T1) opp+id) is non empty set
B2 is Element of the carrier of ((subrelstr T1) opp+id)
[#] ((subrelstr T1) opp+id) is non empty non proper lower upper inaccessible_by_directed_joins closed_under_directed_sups Element of bool the carrier of ((subrelstr T1) opp+id)
bool the carrier of ((subrelstr T1) opp+id) is non empty set
B1 is Element of the carrier of ((subrelstr T1) opp+id)
the carrier of (subrelstr T1) is non empty set
the InternalRel of ((subrelstr T1) opp+id) is Relation-like the carrier of ((subrelstr T1) opp+id) -defined the carrier of ((subrelstr T1) opp+id) -valued Element of bool [: the carrier of ((subrelstr T1) opp+id), the carrier of ((subrelstr T1) opp+id):]
[: the carrier of ((subrelstr T1) opp+id), the carrier of ((subrelstr T1) opp+id):] is non empty Relation-like set
bool [: the carrier of ((subrelstr T1) opp+id), the carrier of ((subrelstr T1) opp+id):] is non empty set
RelStr(# the carrier of ((subrelstr T1) opp+id), the InternalRel of ((subrelstr T1) opp+id) #) is strict RelStr
(subrelstr T1) ~ is non empty strict RelStr
the carrier of ((subrelstr T1) ~) is non empty set
the InternalRel of ((subrelstr T1) ~) is Relation-like the carrier of ((subrelstr T1) ~) -defined the carrier of ((subrelstr T1) ~) -valued Element of bool [: the carrier of ((subrelstr T1) ~), the carrier of ((subrelstr T1) ~):]
[: the carrier of ((subrelstr T1) ~), the carrier of ((subrelstr T1) ~):] is non empty Relation-like set
bool [: the carrier of ((subrelstr T1) ~), the carrier of ((subrelstr T1) ~):] is non empty set
RelStr(# the carrier of ((subrelstr T1) ~), the InternalRel of ((subrelstr T1) ~) #) is strict RelStr
B2 is Element of the carrier of L
a is Element of the carrier of L
A is Element of the carrier of L
Y1 is Element of the carrier of ((subrelstr T1) opp+id)
p is Element of the carrier of (subrelstr T1)
p ~ is Element of the carrier of ((subrelstr T1) ~)
a is Element of the carrier of (subrelstr T1)
a ~ is Element of the carrier of ((subrelstr T1) ~)
Y is Element of the carrier of (subrelstr T1)
Y ~ is Element of the carrier of ((subrelstr T1) ~)
L is non empty reflexive RelStr
the carrier of L is non empty set
bool the carrier of L is non empty set
T1 is non empty filtered Element of bool the carrier of L
(L,T1) is non empty reflexive strict NetStr over L
subrelstr T1 is non empty strict reflexive full SubRelStr of L
(L,(subrelstr T1)) is non empty Relation-like the carrier of (subrelstr T1) -defined the carrier of L -valued Function-like V27( the carrier of (subrelstr T1)) quasi_total monotone Element of bool [: the carrier of (subrelstr T1), the carrier of L:]
the carrier of (subrelstr T1) is non empty set
[: the carrier of (subrelstr T1), the carrier of L:] is non empty Relation-like set
bool [: the carrier of (subrelstr T1), the carrier of L:] is non empty set
(subrelstr T1) opp+id is non empty reflexive strict strict directed antitone antitone eventually-filtered eventually-filtered NetStr over subrelstr T1
(L,(subrelstr T1)) * ((subrelstr T1) opp+id) is non empty reflexive strict directed NetStr over L
L is TopSpace-like TopStruct
the topology of L is quasi_basis quasi_prebasis Element of bool (bool the carrier of L)
the carrier of L is set
bool the carrier of L is non empty set
bool (bool the carrier of L) is non empty set
L is non empty trivial finite 1 -element TopSpace-like discrete V129() V130() V131() V132() TopStruct
the topology of L is finite V46() quasi_basis quasi_prebasis Element of bool (bool the carrier of L)
the carrier of L is non empty trivial finite V49(1) set
bool the carrier of L is non empty finite V46() set
bool (bool the carrier of L) is non empty finite V46() set
bool the carrier of L is non empty finite V46() Element of bool (bool the carrier of L)
T1 is Element of the carrier of L
{T1} is non empty trivial finite V49(1) Element of bool the carrier of L
bool {T1} is non empty finite V46() Element of bool (bool {T1})
bool {T1} is non empty finite V46() set
bool (bool {T1}) is non empty finite V46() set
{{},{T1}} is non empty finite V46() set
T2 is Element of the carrier of L
{T2} is non empty trivial finite V49(1) Element of bool the carrier of L
{{},{T2}} is non empty finite V46() set
L is non empty trivial finite 1 -element TopSpace-like discrete V129() V130() V131() V132() TopStruct
the carrier of L is non empty trivial finite V49(1) set
{ the carrier of L} is non empty trivial finite V46() V49(1) set
bool the carrier of L is non empty finite V46() set
bool (bool the carrier of L) is non empty finite V46() set
the topology of L is finite V46() quasi_basis quasi_prebasis Element of bool (bool the carrier of L)
bool the carrier of L is non empty finite V46() Element of bool (bool the carrier of L)
the Element of the carrier of L is Element of the carrier of L
{ the Element of the carrier of L} is non empty trivial finite V49(1) Element of bool the carrier of L
{{},{ the Element of the carrier of L}} is non empty finite V46() set
T2 is finite V46() Element of bool (bool the carrier of L)
UniCl T2 is finite V46() Element of bool (bool the carrier of L)
B1 is set
{{ the Element of the carrier of L}} is non empty trivial finite V46() V49(1) Element of bool (bool the carrier of L)
union {{ the Element of the carrier of L}} is trivial finite Element of bool the carrier of L
B2 is finite V46() Element of bool (bool the carrier of L)
FinMeetCl B2 is non empty finite V46() Element of bool (bool the carrier of L)
B1 is set
Intersect B2 is trivial finite Element of bool the carrier of L
B1 is finite V46() Element of bool (bool the carrier of L)
FinMeetCl B1 is non empty finite V46() Element of bool (bool the carrier of L)
B2 is set
Intersect B2 is trivial finite Element of bool the carrier of L
L is set
bool L is non empty set
bool (bool L) is non empty set
T1 is set
{T1} is non empty trivial finite V49(1) set
{T1,L} is non empty finite set
{T1,{}} is non empty finite set
T2 is Element of bool (bool L)
FinMeetCl T2 is non empty Element of bool (bool L)
UniCl T2 is Element of bool (bool L)
B1 is set
B2 is Element of bool (bool L)
Intersect B2 is Element of bool L
meet {T1} is set
B1 is Element of bool (bool L)
B1 is set
meet {T1} is set
B2 is Element of bool (bool L)
Intersect B2 is Element of bool L
Intersect T2 is Element of bool L
B1 is set
B2 is Element of bool (bool L)
union B2 is Element of bool L
B1 is set
union B2 is Element of bool L
union T2 is Element of bool L
L is set
bool L is non empty set
bool (bool L) is non empty set
{L} is non empty trivial finite V49(1) set
T1 is Element of bool (bool L)
T2 is Element of bool (bool L)
T2 \/ {L} is non empty set
T1 \ {L} is Element of bool (bool L)
Intersect T1 is Element of bool L
Intersect T2 is Element of bool L
B1 is set
B2 is set
B1 is set
B2 is set
L is set
bool L is non empty set
bool (bool L) is non empty set
{L} is non empty trivial finite V49(1) set
T1 is Element of bool (bool L)
T2 is Element of bool (bool L)
T2 \/ {L} is non empty set
T1 \ {L} is Element of bool (bool L)
FinMeetCl T1 is non empty Element of bool (bool L)
FinMeetCl T2 is non empty Element of bool (bool L)
(T1 \ {L}) \/ {L} is non empty set
T1 \/ {L} is non empty set
FinMeetCl (FinMeetCl T2) is non empty Element of bool (bool L)
L is set
bool L is non empty set
bool (bool L) is non empty set
T1 is Element of bool (bool L)
FinMeetCl T1 is non empty Element of bool (bool L)
{L} is non empty trivial finite V49(1) set
T2 is non empty finite Element of bool (bool L)
B1 is non empty finite Element of bool (bool L)
Intersect B1 is Element of bool L
meet B1 is Element of bool L
B2 is set
B1 is Element of bool (bool L)
Intersect B1 is Element of bool L
B1 is non empty finite Element of bool (bool L)
Intersect B1 is Element of bool L
L is set
bool L is non empty set
bool (bool L) is non empty set
T1 is Element of bool (bool L)
UniCl T1 is Element of bool (bool L)
UniCl (UniCl T1) is Element of bool (bool L)
T2 is set
B1 is Element of bool (bool L)
union B1 is Element of bool L
{ b₁ where b₁ is Element of bool L : ( b₁ in T1 & b₁ c= T2 ) } is set
bool L is non empty Element of bool (bool L)
B1 is set
B2 is Element of bool L
B1 is Element of bool (bool L)
union B1 is Element of bool L
B2 is set
a is set
A is Element of bool (bool L)
union A is Element of bool L
p is set
a is Element of bool L
B2 is set
a is set
A is Element of bool L
B2 is set
a is Element of bool L
L is set
bool L is non empty set
bool (bool L) is non empty set
T1 is empty proper Relation-like non-empty empty-yielding Function-like one-to-one constant functional V35() V36() V37() V39() V40() V41() finite finite-yielding V46() V47() V49( {} ) Element of bool (bool L)
UniCl T1 is Element of bool (bool L)
T2 is set
B1 is Element of bool (bool L)
union B1 is Element of bool L
T2 is set
bool L is non empty Element of bool (bool L)
{} (bool L) is empty proper Relation-like non-empty empty-yielding Function-like one-to-one constant functional V35() V36() V37() V39() V40() V41() finite finite-yielding V46() V47() V49( {} ) Element of bool (bool L)
bool (bool L) is non empty set
union ({} (bool L)) is V35() V36() V37() V41() finite V47() Element of bool L
L is set
bool L is non empty set
bool (bool L) is non empty set
{L} is non empty trivial finite V49(1) set
T1 is empty proper Relation-like non-empty empty-yielding Function-like one-to-one constant functional V35() V36() V37() V39() V40() V41() finite finite-yielding V46() V47() V49( {} ) Element of bool (bool L)
FinMeetCl T1 is non empty Element of bool (bool L)
T2 is set
B1 is Element of bool (bool L)
Intersect B1 is Element of bool L
T2 is set
bool L is non empty Element of bool (bool L)
{} (bool L) is empty proper Relation-like non-empty empty-yielding Function-like one-to-one constant functional V35() V36() V37() V39() V40() V41() finite finite-yielding V46() V47() V49( {} ) Element of bool (bool L)
bool (bool L) is non empty set
Intersect ({} (bool L)) is Element of bool L
L is set
bool L is non empty set
bool (bool L) is non empty set
{{},L} is non empty finite set
T1 is Element of bool (bool L)
UniCl T1 is Element of bool (bool L)
FinMeetCl T1 is non empty Element of bool (bool L)
T2 is set
B1 is Element of bool (bool L)
union B1 is Element of bool L
{L} is non empty trivial finite V49(1) set
{} \/ L is set
T2 is set
B1 is Element of bool (bool L)
Intersect B1 is Element of bool L
meet {{}} is set
meet {L} is set
meet {{},L} is set
{} /\ L is Relation-like finite set
L is set
bool L is non empty set
bool (bool L) is non empty set
T1 is set
bool T1 is non empty set
bool (bool T1) is non empty set
T2 is Element of bool (bool L)
UniCl T2 is Element of bool (bool L)
B1 is Element of bool (bool T1)
UniCl B1 is Element of bool (bool T1)
B2 is set
bool B2 is non empty set
bool (bool B2) is non empty set
B1 is set
bool B1 is non empty set
bool (bool B1) is non empty set
B2 is Element of bool (bool B2)
a is Element of bool (bool B1)
UniCl B2 is Element of bool (bool B2)
UniCl a is Element of bool (bool B1)
A is set
p is Element of bool (bool B2)
union p is Element of bool B2
a is Element of bool (bool B1)
union a is Element of bool B1
L is set
bool L is non empty set
bool (bool L) is non empty set
T1 is set
bool T1 is non empty set
bool (bool T1) is non empty set
{T1} is non empty trivial finite V49(1) set
T2 is Element of bool (bool L)
FinMeetCl T2 is non empty Element of bool (bool L)
{T1} \/ (FinMeetCl T2) is non empty set
B1 is Element of bool (bool T1)
FinMeetCl B1 is non empty Element of bool (bool T1)
B2 is set
B1 is Element of bool (bool T1)
Intersect B1 is Element of bool T1
B2 is Element of bool (bool L)
meet B1 is Element of bool T1
a is Element of bool (bool L)
Intersect a is Element of bool L
B2 is set
bool T1 is non empty Element of bool (bool T1)
{} (bool T1) is empty proper Relation-like non-empty empty-yielding Function-like one-to-one constant functional V35() V36() V37() V39() V40() V41() finite finite-yielding V46() V47() V49( {} ) Element of bool (bool T1)
bool (bool T1) is non empty set
Intersect ({} (bool T1)) is Element of bool T1
B1 is non empty finite Element of bool (bool L)
Intersect B1 is Element of bool L
B2 is Element of bool (bool T1)
a is Element of bool (bool T1)
meet a is Element of bool T1
Intersect a is Element of bool T1
L is set
bool L is non empty set
bool (bool L) is non empty set
T1 is Element of bool (bool L)
UniCl T1 is Element of bool (bool L)
FinMeetCl (UniCl T1) is non empty Element of bool (bool L)
UniCl (FinMeetCl (UniCl T1)) is Element of bool (bool L)
FinMeetCl T1 is non empty Element of bool (bool L)
UniCl (FinMeetCl T1) is Element of bool (bool L)
{L} is non empty trivial finite V49(1) set
{{},L} is non empty finite set
{L,{}} is non empty finite set
T2 is non empty Element of bool (bool L)
UniCl T2 is Element of bool (bool L)
FinMeetCl (UniCl T2) is non empty Element of bool (bool L)
UniCl (FinMeetCl (UniCl T2)) is Element of bool (bool L)
FinMeetCl T2 is non empty Element of bool (bool L)
UniCl (FinMeetCl T2) is Element of bool (bool L)
UniCl (UniCl (FinMeetCl T2)) is Element of bool (bool L)
B1 is set
B2 is Element of bool (bool L)
union B2 is Element of bool L
B1 is set
B2 is Element of bool (bool L)
Intersect B2 is Element of bool L
meet B2 is Element of bool L
Funcs (B2,T2) is non empty functional FUNCTION_DOMAIN of B2,T2
{ (meet (rng b₁)) where b₁ is Relation-like B2 -defined T2 -valued Function-like V27(B2) quasi_total Element of Funcs (B2,T2) : for b₂ being set holds
( not b₂ in B2 or b₁ . b₂ c= b₂ ) } is set
A is set
p is Relation-like B2 -defined T2 -valued Function-like V27(B2) quasi_total Element of Funcs (B2,T2)
rng p is Element of bool T2
bool T2 is non empty set
meet (rng p) is set
a is Element of bool (bool L)
Y is Element of bool (bool L)
Intersect Y is Element of bool L
A is Element of bool (bool L)
p is Element of bool (bool L)
union p is Element of bool L
a is set
Y is set
Y1 is Relation-like B2 -defined T2 -valued Function-like V27(B2) quasi_total Element of Funcs (B2,T2)
rng Y1 is Element of bool T2
bool T2 is non empty set
meet (rng Y1) is set
dom Y1 is Element of bool B2
bool B2 is non empty set
Y2 is Element of bool (bool L)
cT2 is set
Z1 is set
Y1 . Z1 is set
cT1 is Element of bool (bool L)
a is set
Y is set
Y1 is Element of bool (bool L)
union Y1 is Element of bool L
Y2 is set
cT1 is set
Y is Relation-like Function-like set
dom Y is set
rng Y is set
Y1 is Relation-like B2 -defined T2 -valued Function-like V27(B2) quasi_total Element of Funcs (B2,T2)
Y2 is set
Y1 . Y2 is set
rng Y1 is Element of bool T2
meet (rng Y1) is set
Y2 is set
cT1 is set
Y1 . cT1 is set
L is TopSpace-like TopStruct
the carrier of L is set
bool the carrier of L is non empty set
bool (bool the carrier of L) is non empty set
the topology of L is quasi_basis quasi_prebasis Element of bool (bool the carrier of L)
T1 is Element of bool (bool the carrier of L)
UniCl T1 is Element of bool (bool the carrier of L)
UniCl the topology of L is Element of bool (bool the carrier of L)
L is TopSpace-like TopStruct
the carrier of L is set
bool the carrier of L is non empty set
bool (bool the carrier of L) is non empty set
T1 is Element of bool (bool the carrier of L)
FinMeetCl T1 is non empty Element of bool (bool the carrier of L)
the topology of L is quasi_basis quasi_prebasis Element of bool (bool the carrier of L)
bool the carrier of L is non empty Element of bool (bool the carrier of L)
FinMeetCl the topology of L is non empty Element of bool (bool the carrier of L)
T2 is open quasi_basis quasi_prebasis Element of bool (bool the carrier of L)
UniCl T2 is Element of bool (bool the carrier of L)
UniCl (FinMeetCl T1) is Element of bool (bool the carrier of L)
L is non empty TopSpace-like TopStruct
the carrier of L is non empty set
bool the carrier of L is non empty set
bool (bool the carrier of L) is non empty set
T1 is Element of bool (bool the carrier of L)
UniCl T1 is Element of bool (bool the carrier of L)
FinMeetCl (UniCl T1) is non empty Element of bool (bool the carrier of L)
UniCl (FinMeetCl (UniCl T1)) is Element of bool (bool the carrier of L)
the topology of L is quasi_basis quasi_prebasis Element of bool (bool the carrier of L)
FinMeetCl T1 is non empty Element of bool (bool the carrier of L)
UniCl (FinMeetCl T1) is Element of bool (bool the carrier of L)
L is TopSpace-like TopStruct
the carrier of L is set
bool the carrier of L is non empty set
bool (bool the carrier of L) is non empty set
T1 is TopSpace-like TopStruct
the carrier of T1 is set
bool the carrier of T1 is non empty set
bool (bool the carrier of T1) is non empty set
the topology of L is quasi_basis quasi_prebasis Element of bool (bool the carrier of L)
the topology of T1 is quasi_basis quasi_prebasis Element of bool (bool the carrier of T1)
T2 is open quasi_basis quasi_prebasis Element of bool (bool the carrier of L)
B1 is open quasi_basis quasi_prebasis Element of bool (bool the carrier of T1)
UniCl B1 is Element of bool (bool the carrier of T1)
L is TopSpace-like TopStruct
the carrier of L is set
bool the carrier of L is non empty set
bool (bool the carrier of L) is non empty set
T1 is TopSpace-like TopStruct
the carrier of T1 is set
bool the carrier of T1 is non empty set
bool (bool the carrier of T1) is non empty set
the topology of L is quasi_basis quasi_prebasis Element of bool (bool the carrier of L)
the topology of T1 is quasi_basis quasi_prebasis Element of bool (bool the carrier of T1)
T2 is open quasi_prebasis Element of bool (bool the carrier of L)
FinMeetCl T2 is non empty Element of bool (bool the carrier of L)
B1 is open quasi_prebasis Element of bool (bool the carrier of T1)
FinMeetCl B1 is non empty Element of bool (bool the carrier of T1)
L is TopSpace-like TopStruct
the carrier of L is set
bool the carrier of L is non empty set
bool (bool the carrier of L) is non empty set
T2 is TopSpace-like TopStruct
the carrier of T2 is set
bool the carrier of T2 is non empty set
bool (bool the carrier of T2) is non empty set
T1 is open quasi_basis quasi_prebasis Element of bool (bool the carrier of L)
B1 is open quasi_basis quasi_prebasis Element of bool (bool the carrier of T2)
L is TopSpace-like TopStruct
the carrier of L is set
bool the carrier of L is non empty set
bool (bool the carrier of L) is non empty set
T1 is open quasi_prebasis Element of bool (bool the carrier of L)
L is non empty TopSpace-like TopStruct
the carrier of L is non empty set
bool the carrier of L is non empty set
bool (bool the carrier of L) is non empty set
{ the carrier of L} is non empty trivial finite V49(1) set
T1 is open quasi_prebasis Element of bool (bool the carrier of L)
T1 \/ { the carrier of L} is non empty set
the topology of L is quasi_basis quasi_prebasis Element of bool (bool the carrier of L)
B1 is Element of bool (bool the carrier of L)
FinMeetCl T1 is non empty Element of bool (bool the carrier of L)
FinMeetCl B1 is non empty Element of bool (bool the carrier of L)
L is TopSpace-like TopStruct
the carrier of L is set
bool the carrier of L is non empty set
bool (bool the carrier of L) is non empty set
{ the carrier of L} is non empty trivial finite V49(1) set
T1 is open quasi_basis quasi_prebasis Element of bool (bool the carrier of L)
T1 \/ { the carrier of L} is non empty set
the topology of L is quasi_basis quasi_prebasis Element of bool (bool the carrier of L)
B1 is Element of bool (bool the carrier of L)
UniCl T1 is Element of bool (bool the carrier of L)
UniCl B1 is Element of bool (bool the carrier of L)
L is TopSpace-like TopStruct
the carrier of L is set
bool the carrier of L is non empty set
bool (bool the carrier of L) is non empty set
T1 is open quasi_basis quasi_prebasis Element of bool (bool the carrier of L)
T2 is Element of bool the carrier of L
{ b₁ where b₁ is Element of bool the carrier of L : ( b₁ in T1 & b₁ c= T2 ) } is set
union { b₁ where b₁ is Element of bool the carrier of L : ( b₁ in T1 & b₁ c= T2 ) } is set
B1 is Element of the carrier of L
B2 is set
B1 is Element of bool the carrier of L
bool the carrier of L is non empty Element of bool (bool the carrier of L)
B2 is set
B1 is Element of bool the carrier of L
B2 is Element of bool (bool the carrier of L)
B1 is Element of bool (bool the carrier of L)
B2 is Element of bool the carrier of L
the topology of L is quasi_basis quasi_prebasis Element of bool (bool the carrier of L)
a is Element of bool the carrier of L
union B1 is Element of bool the carrier of L
B2 is set
a is Element of the carrier of L
A is Element of bool the carrier of L
bool T2 is non empty Element of bool (bool T2)
bool T2 is non empty set
bool (bool T2) is non empty set
B2 is set
a is Element of bool the carrier of L
union (bool T2) is Element of bool T2
L is TopSpace-like TopStruct
the carrier of L is set
bool the carrier of L is non empty set
bool (bool the carrier of L) is non empty set
the topology of L is quasi_basis quasi_prebasis Element of bool (bool the carrier of L)
T1 is Element of bool (bool the carrier of L)
T2 is set
UniCl T1 is Element of bool (bool the carrier of L)
B1 is Element of bool the carrier of L
{ b₁ where b₁ is Element of bool the carrier of L : ( b₁ in T1 & b₁ c= B1 ) } is set
bool the carrier of L is non empty Element of bool (bool the carrier of L)
B1 is set
B2 is Element of bool the carrier of L
B1 is Element of bool (bool the carrier of L)
B2 is set
a is Element of bool the carrier of L
union B1 is Element of bool the carrier of L
B2 is set
a is Element of the carrier of L
A is Element of bool the carrier of L
B2 is set
a is set
A is Element of bool the carrier of L
L is TopSpace-like TopStruct
the carrier of L is set
T1 is non empty TopSpace-like TopStruct
the carrier of T1 is non empty set
bool the carrier of T1 is non empty set
bool (bool the carrier of T1) is non empty set
[: the carrier of L, the carrier of T1:] is Relation-like set
bool [: the carrier of L, the carrier of T1:] is non empty set
T2 is open quasi_basis quasi_prebasis Element of bool (bool the carrier of T1)
B1 is Relation-like the carrier of L -defined the carrier of T1 -valued Function-like V27( the carrier of L) quasi_total Element of bool [: the carrier of L, the carrier of T1:]
the topology of T1 is quasi_basis quasi_prebasis Element of bool (bool the carrier of T1)
B2 is Element of bool the carrier of T1
B2 ` is Element of bool the carrier of T1
B1 " (B2 `) is Element of bool the carrier of L
bool the carrier of L is non empty set
B2 is Element of bool the carrier of T1
B1 " B2 is Element of bool the carrier of L
B2 ` is Element of bool the carrier of T1
{ b<sub>1</sub> where b<sub>1</sub> is Element of bool the carrier of T1 : ( b<sub>1</sub> in T2 & b<sub>1</sub> c= B2 ` ) } is set
union { b₁ where b₁ is Element of bool the carrier of T1 : ( b₁ in T2 & b₁ c= B2 ` ) } is set
{ (B1 " b<sub>1</sub>) where b<sub>1</sub> is Element of bool the carrier of T1 : ( b<sub>1</sub> in T2 & b<sub>1</sub> c= B2 ` ) } is set
bool the carrier of L is non empty Element of bool (bool the carrier of L)
bool (bool the carrier of L) is non empty set
B2 is set
a is Element of bool the carrier of T1
B1 " a is Element of bool the carrier of L
B2 is Element of bool (bool the carrier of L)
a is Element of bool (bool the carrier of L)
the topology of L is quasi_basis quasi_prebasis Element of bool (bool the carrier of L)
A is set
p is Element of bool the carrier of T1
B1 " p is Element of bool the carrier of L
p ` is Element of bool the carrier of T1
B1 " (p `) is Element of bool the carrier of L
(B1 " p) ` is Element of bool the carrier of L
union a is Element of bool the carrier of L
{ H<sub>1</sub>(b<sub>1</sub>) where b<sub>1</sub> is Element of bool the carrier of T1 : S<sub>1</sub>[b<sub>1</sub>] } is set
union { H<sub>1</sub>(b<sub>1</sub>) where b<sub>1</sub> is Element of bool the carrier of T1 : S<sub>1</sub>[b<sub>1</sub>] } is set
B1 " (union { H<sub>1</sub>(b<sub>1</sub>) where b<sub>1</sub> is Element of bool the carrier of T1 : S<sub>1</sub>[b<sub>1</sub>] } ) is Element of bool the carrier of L
{ (B1 " H<sub>1</sub>(b<sub>1</sub>)) where b<sub>1</sub> is Element of bool the carrier of T1 : S<sub>1</sub>[b<sub>1</sub>] } is set
union { (B1 " H<sub>1</sub>(b<sub>1</sub>)) where b<sub>1</sub> is Element of bool the carrier of T1 : S<sub>1</sub>[b<sub>1</sub>] } is set
B1 " (B2 `) is Element of bool the carrier of L
(B1 " B2) ` is Element of bool the carrier of L
L is TopSpace-like TopStruct
the carrier of L is set
T1 is non empty TopSpace-like TopStruct
the carrier of T1 is non empty set
bool the carrier of T1 is non empty set
bool (bool the carrier of T1) is non empty set
[: the carrier of L, the carrier of T1:] is Relation-like set
bool [: the carrier of L, the carrier of T1:] is non empty set
T2 is open quasi_basis quasi_prebasis Element of bool (bool the carrier of T1)
B1 is Relation-like the carrier of L -defined the carrier of T1 -valued Function-like V27( the carrier of L) quasi_total Element of bool [: the carrier of L, the carrier of T1:]
B2 is Element of bool the carrier of T1
B2 ` is Element of bool the carrier of T1
B1 " (B2 `) is Element of bool the carrier of L
bool the carrier of L is non empty set
B1 " B2 is Element of bool the carrier of L
(B1 " B2) ` is Element of bool the carrier of L
B2 is Element of bool the carrier of T1
B1 " B2 is Element of bool the carrier of L
(B1 " B2) ` is Element of bool the carrier of L
B2 ` is Element of bool the carrier of T1
B1 " (B2 `) is Element of bool the carrier of L
L is TopSpace-like TopStruct
the carrier of L is set
T1 is non empty TopSpace-like TopStruct
the carrier of T1 is non empty set
bool the carrier of T1 is non empty set
bool (bool the carrier of T1) is non empty set
[: the carrier of L, the carrier of T1:] is Relation-like set
bool [: the carrier of L, the carrier of T1:] is non empty set
T2 is open quasi_prebasis Element of bool (bool the carrier of T1)
B1 is Relation-like the carrier of L -defined the carrier of T1 -valued Function-like V27( the carrier of L) quasi_total Element of bool [: the carrier of L, the carrier of T1:]
the topology of T1 is quasi_basis quasi_prebasis Element of bool (bool the carrier of T1)
B2 is Element of bool the carrier of T1
B2 ` is Element of bool the carrier of T1
B1 " (B2 `) is Element of bool the carrier of L
bool the carrier of L is non empty set
FinMeetCl T2 is non empty Element of bool (bool the carrier of T1)
B1 is Element of bool the carrier of T1
B2 is open quasi_basis quasi_prebasis Element of bool (bool the carrier of T1)
B2 is Element of bool (bool the carrier of T1)
Intersect B2 is Element of bool the carrier of T1
a is Element of bool (bool the carrier of T1)
COMPLEMENT a is Element of bool (bool the carrier of T1)
B1 ` is Element of bool the carrier of T1
B1 " (B1 `) is Element of bool the carrier of L
A is Element of bool (bool the carrier of T1)
union A is Element of bool the carrier of T1
B1 " (union A) is Element of bool the carrier of L
{ H<sub>1</sub>(b<sub>1</sub>) where b<sub>1</sub> is Element of bool the carrier of T1 : S<sub>1</sub>[b<sub>1</sub>] } is set
union { H<sub>1</sub>(b<sub>1</sub>) where b<sub>1</sub> is Element of bool the carrier of T1 : S<sub>1</sub>[b<sub>1</sub>] } is set
B1 " (union { H<sub>1</sub>(b<sub>1</sub>) where b<sub>1</sub> is Element of bool the carrier of T1 : S<sub>1</sub>[b<sub>1</sub>] } ) is Element of bool the carrier of L
{ (B1 " H<sub>1</sub>(b<sub>1</sub>)) where b<sub>1</sub> is Element of bool the carrier of T1 : S<sub>1</sub>[b<sub>1</sub>] } is set
union { (B1 " H<sub>1</sub>(b<sub>1</sub>)) where b<sub>1</sub> is Element of bool the carrier of T1 : S<sub>1</sub>[b<sub>1</sub>] } is set
{ (B1 " (b<sub>1</sub> `)) where b₁ is Element of bool the carrier of T1 : b₁ in a } is set
bool the carrier of L is non empty Element of bool (bool the carrier of L)
bool (bool the carrier of L) is non empty set
a is set
Y is Element of bool the carrier of T1
Y ` is Element of bool the carrier of T1
B1 " (Y `) is Element of bool the carrier of L
a is Element of bool (bool the carrier of L)
Y is Element of bool (bool the carrier of L)
Y1 is Element of bool the carrier of L
Y2 is Element of bool the carrier of T1
Y2 ` is Element of bool the carrier of T1
B1 " (Y2 `) is Element of bool the carrier of L
{ H₂(b₁) where b₁ is Element of bool the carrier of T1 : b₁ in a } is set
L is TopSpace-like TopStruct
the carrier of L is set
T1 is non empty TopSpace-like TopStruct
the carrier of T1 is non empty set
bool the carrier of T1 is non empty set
bool (bool the carrier of T1) is non empty set
[: the carrier of L, the carrier of T1:] is Relation-like set
bool [: the carrier of L, the carrier of T1:] is non empty set
T2 is open quasi_prebasis Element of bool (bool the carrier of T1)
B1 is Relation-like the carrier of L -defined the carrier of T1 -valued Function-like V27( the carrier of L) quasi_total Element of bool [: the carrier of L, the carrier of T1:]
B2 is Element of bool the carrier of T1
B2 ` is Element of bool the carrier of T1
B1 " (B2 `) is Element of bool the carrier of L
bool the carrier of L is non empty set
B1 " B2 is Element of bool the carrier of L
(B1 " B2) ` is Element of bool the carrier of L
B2 is Element of bool the carrier of T1
B1 " B2 is Element of bool the carrier of L
(B1 " B2) ` is Element of bool the carrier of L
B2 ` is Element of bool the carrier of T1
B1 " (B2 `) is Element of bool the carrier of L
L is non empty TopSpace-like TopStruct
the carrier of L is non empty set
bool the carrier of L is non empty set
bool (bool the carrier of L) is non empty set
T1 is Element of the carrier of L
T2 is Element of bool the carrier of L
Cl T2 is Element of bool the carrier of L
B1 is open quasi_basis quasi_prebasis Element of bool (bool the carrier of L)
B2 is a_neighborhood of T1
Int B2 is Element of bool the carrier of L
{ b₁ where b₁ is Element of bool the carrier of L : ( b₁ in B1 & b₁ c= B2 ) } is set
union { b₁ where b₁ is Element of bool the carrier of L : ( b₁ in B1 & b₁ c= B2 ) } is set
B1 is set
B2 is Element of bool the carrier of L
L is non empty TopSpace-like TopStruct
the carrier of L is non empty set
bool the carrier of L is non empty set
bool (bool the carrier of L) is non empty set
T1 is Element of the carrier of L
T2 is Element of bool the carrier of L
Cl T2 is Element of bool the carrier of L
B1 is open quasi_prebasis Element of bool (bool the carrier of L)
FinMeetCl B1 is non empty Element of bool (bool the carrier of L)
B1 is Element of bool the carrier of L
B2 is open quasi_basis quasi_prebasis Element of bool (bool the carrier of L)
B2 is Element of bool (bool the carrier of L)
Intersect B2 is Element of bool the carrier of L
L is non empty TopSpace-like TopStruct
the carrier of L is non empty set
bool the carrier of L is non empty set
bool (bool the carrier of L) is non empty set
T1 is open quasi_prebasis Element of bool (bool the carrier of L)
T2 is Element of the carrier of L
B1 is non empty transitive directed NetStr over L
netmap (B1,L) is non empty Relation-like the carrier of B1 -defined the carrier of L -valued Function-like V27( the carrier of B1) quasi_total Element of bool [: the carrier of B1, the carrier of L:]
the carrier of B1 is non empty set
[: the carrier of B1, the carrier of L:] is non empty Relation-like set
bool [: the carrier of B1, the carrier of L:] is non empty set
the mapping of B1 is non empty Relation-like the carrier of B1 -defined the carrier of L -valued Function-like V27( the carrier of B1) quasi_total Element of bool [: the carrier of B1, the carrier of L:]
rng (netmap (B1,L)) is non empty Element of bool the carrier of L
B2 is Element of bool the carrier of L
Cl B2 is Element of bool the carrier of L
[#] B1 is non empty non proper lower upper Element of bool the carrier of B1
bool the carrier of B1 is non empty set
B1 is finite Element of bool (bool the carrier of L)
Intersect B1 is Element of bool the carrier of L
B2 is set
a is Element of bool the carrier of L
A is Element of the carrier of B1
p is set
a is set
Y is Element of the carrier of B1
Y1 is Element of the carrier of B1
B1 . Y1 is Element of the carrier of L
the mapping of B1 . Y1 is Element of the carrier of L
B2 is Relation-like Function-like set
dom B2 is set
rng B2 is set
the Element of the carrier of B1 is Element of the carrier of B1
B1 . the Element of the carrier of B1 is Element of the carrier of L
the mapping of B1 . the Element of the carrier of B1 is Element of the carrier of L
A is non empty finite Element of bool the carrier of B1
p is Element of the carrier of B1
a is set
B2 . a is set
Y is Element of the carrier of B1
B1 . p is Element of the carrier of L
the mapping of B1 . p is Element of the carrier of L
L is non empty TopSpace-like TopStruct
the carrier of L is non empty set
bool the carrier of L is non empty set
bool (bool the carrier of L) is non empty set
T1 is non empty TopSpace-like TopStruct
the carrier of T1 is non empty set
bool the carrier of T1 is non empty set
bool (bool the carrier of T1) is non empty set
[:L,T1:] is non empty strict TopSpace-like TopStruct
the carrier of [:L,T1:] is non empty set
bool the carrier of [:L,T1:] is non empty set
bool (bool the carrier of [:L,T1:]) is non empty set
T2 is open quasi_basis quasi_prebasis Element of bool (bool the carrier of L)
B1 is open quasi_basis quasi_prebasis Element of bool (bool the carrier of T1)
{ [:b₁,b₂:] where b₁ is Element of bool the carrier of L, b₂ is Element of bool the carrier of T1 : ( b₁ in T2 & b₂ in B1 ) } is set
[: the carrier of L, the carrier of T1:] is non empty Relation-like set
bool the carrier of [:L,T1:] is non empty Element of bool (bool the carrier of [:L,T1:])
B2 is set
a is Element of bool the carrier of L
A is Element of bool the carrier of T1
[:a,A:] is Relation-like Element of bool the carrier of [:L,T1:]
the topology of L is quasi_basis quasi_prebasis Element of bool (bool the carrier of L)
the topology of T1 is quasi_basis quasi_prebasis Element of bool (bool the carrier of T1)
B2 is Element of bool (bool the carrier of [:L,T1:])
a is Element of bool the carrier of [:L,T1:]
A is Element of bool the carrier of L
p is Element of bool the carrier of T1
[:A,p:] is Relation-like Element of bool the carrier of [:L,T1:]
a is set
the topology of [:L,T1:] is quasi_basis quasi_prebasis Element of bool (bool the carrier of [:L,T1:])
UniCl B2 is Element of bool (bool the carrier of [:L,T1:])
A is Element of bool the carrier of [:L,T1:]
Base-Appr A is open Element of bool (bool the carrier of [:L,T1:])
union (Base-Appr A) is Element of bool the carrier of [:L,T1:]
B2 /\ (Base-Appr A) is Element of bool (bool the carrier of [:L,T1:])
a is Element of bool (bool the carrier of [:L,T1:])
union a is Element of bool the carrier of [:L,T1:]
Y is set
Y1 is Element of the carrier of [:L,T1:]
Y2 is set
cT1 is set
[Y2,cT1] is set
{Y2,cT1} is non empty finite set
{Y2} is non empty trivial finite V49(1) set
{{Y2,cT1},{Y2}} is non empty finite V46() set
z1 is set
{ [:b₁,b₂:] where b₁ is Element of bool the carrier of L, b₂ is Element of bool the carrier of T1 : ( [:b₁,b₂:] c= A & b₁ is open & b₂ is open ) } is set
Z2 is Element of bool the carrier of L
z2 is Element of bool the carrier of T1
[:Z2,z2:] is Relation-like Element of bool the carrier of [:L,T1:]
cT2 is Element of the carrier of L
Z1 is Element of the carrier of T1
p2 is Element of bool the carrier of L
b is Element of bool the carrier of T1
[:p2,b:] is Relation-like Element of bool the carrier of [:L,T1:]
L is non empty TopSpace-like TopStruct
the carrier of L is non empty set
bool the carrier of L is non empty set
bool (bool the carrier of L) is non empty set
T1 is non empty TopSpace-like TopStruct
the carrier of T1 is non empty set
bool the carrier of T1 is non empty set
bool (bool the carrier of T1) is non empty set
[:L,T1:] is non empty strict TopSpace-like TopStruct
the carrier of [:L,T1:] is non empty set
bool the carrier of [:L,T1:] is non empty set
bool (bool the carrier of [:L,T1:]) is non empty set
B1 is open quasi_prebasis Element of bool (bool the carrier of L)
{ [:b₁, the carrier of T1:] where b₁ is Element of bool the carrier of L : b₁ in B1 } is set
B2 is open quasi_prebasis Element of bool (bool the carrier of T1)
{ [: the carrier of L,b₁:] where b₁ is Element of bool the carrier of T1 : b₁ in B2 } is set
{ [: the carrier of L,b₁:] where b₁ is Element of bool the carrier of T1 : b₁ in B2 } \/ { [:b₁, the carrier of T1:] where b₁ is Element of bool the carrier of L : b₁ in B1 } is set
FinMeetCl B1 is non empty Element of bool (bool the carrier of L)
FinMeetCl B2 is non empty Element of bool (bool the carrier of T1)
a is open quasi_basis quasi_prebasis Element of bool (bool the carrier of L)
A is open quasi_basis quasi_prebasis Element of bool (bool the carrier of T1)
{ [:b₁,b₂:] where b₁ is Element of bool the carrier of L, b₂ is Element of bool the carrier of T1 : ( b₁ in a & b₂ in A ) } is set
a is Element of bool the carrier of L
the topology of L is quasi_basis quasi_prebasis Element of bool (bool the carrier of L)
Y is Element of bool the carrier of T1
the topology of T1 is quasi_basis quasi_prebasis Element of bool (bool the carrier of T1)
bool the carrier of [:L,T1:] is non empty Element of bool (bool the carrier of [:L,T1:])
Y1 is set
Y2 is Element of bool the carrier of L
[:Y2,Y:] is Relation-like Element of bool the carrier of [:L,T1:]
Y1 is Element of bool (bool the carrier of [:L,T1:])
cT1 is set
cT2 is Element of bool the carrier of T1
[:a,cT2:] is Relation-like Element of bool the carrier of [:L,T1:]
cT1 is Element of bool (bool the carrier of [:L,T1:])
cT2 is Element of bool (bool the carrier of [:L,T1:])
Y2 is Element of bool (bool the carrier of [:L,T1:])
cT2 \/ Y2 is Element of bool (bool the carrier of [:L,T1:])
Z1 is Element of bool (bool the carrier of [:L,T1:])
z1 is Element of bool the carrier of [:L,T1:]
Z2 is Element of bool the carrier of L
[:Z2,Y:] is Relation-like Element of bool the carrier of [:L,T1:]
z2 is Element of bool the carrier of T1
[:a,z2:] is Relation-like Element of bool the carrier of [:L,T1:]
Z2 is Element of bool the carrier of L
z2 is Element of bool the carrier of T1
[:Z2,z2:] is Relation-like Element of bool the carrier of [:L,T1:]
p is open quasi_basis quasi_prebasis Element of bool (bool the carrier of [:L,T1:])
FinMeetCl Z1 is non empty Element of bool (bool the carrier of [:L,T1:])
z1 is set
Z2 is Element of bool the carrier of L
z2 is Element of bool the carrier of T1
[:Z2,z2:] is Relation-like Element of bool the carrier of [:L,T1:]
p2 is Element of bool (bool the carrier of L)
Intersect p2 is Element of bool the carrier of L
b is Element of bool (bool the carrier of T1)
Intersect b is Element of bool the carrier of T1
{ H₁(b₁) where b₁ is Element of bool the carrier of L : b₁ in p2 } is set
{ H₂(b₁) where b₁ is Element of bool the carrier of T1 : b₁ in b } is set
{ [:b₁,Y:] where b₁ is Element of bool the carrier of L : b₁ in p2 } is set
{ [:a,b₁:] where b₁ is Element of bool the carrier of T1 : b₁ in b } is set
Y is set
Y is Element of bool the carrier of L
[:Y,Y:] is Relation-like Element of bool the carrier of [:L,T1:]
Y is set
Y is Element of