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

bool F

F

F

{ F

{ F

L is set

T1 is Element of F

F

F

L is set

T1 is Element of F

F

T2 is Element of F

F

F

the carrier of F

bool the carrier of F

bool (bool the carrier of F

F

F

{ F

COMPLEMENT F

{ (F

L is set

T1 is Element of bool the carrier of F

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

L is set

T1 is Element of the carrier of F

F

F

F

the carrier of F

bool the carrier of F

bool (bool the carrier of F

F

F

{ (F

COMPLEMENT F

{ F

L is set

T1 is Element of bool the carrier of F

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

F

L is set

T1 is Element of the carrier of F

F

F

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

F

the carrier of F

bool the carrier of F

{ F

union { F

F

{ (F

union { (F

T2 is set

dom F

F

B1 is set

B2 is Element of bool the carrier of F

F

F

T2 is set

B1 is set

B2 is Element of bool the carrier of F

F

F

F

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

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

union { (uparrow b

downarrow T1 is Element of bool the carrier of L

{ (downarrow b

union { (downarrow b

{ b

( b

{ b

( b

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

uparrow T2 is Element of bool the carrier of L

(uparrow T2) ` is Element of bool the carrier of L

{ (H

COMPLEMENT T1 is Element of bool (bool the carrier of L)

{ H

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

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

( not b

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

union { b

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

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

union { b

{ (B1 " b

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

union { H

B1 " (union { H

{ (B1 " H

union { (B1 " H

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

union { H

B1 " (union { H

{ (B1 " H

union { (B1 " H

{ (B1 " (b

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

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

union { b

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

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

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

B2 is open quasi_prebasis Element of bool (bool the carrier of T1)

{ [: the carrier of L,b

{ [: the carrier of L,b

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

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

{ H

{ [:b

{ [:a,b

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