:: WAYBEL_6 semantic presentation

REAL is set

NAT is non empty non trivial epsilon-transitive epsilon-connected ordinal non finite V42() V43() Element of bool REAL

bool REAL is non empty set

NAT is non empty non trivial epsilon-transitive epsilon-connected ordinal non finite V42() V43() set

bool NAT is non empty non trivial non finite set

bool NAT is non empty non trivial non finite set

K257() is L6()

the carrier of K257() is set

{} is empty ext-real non positive non negative epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural Relation-like non-empty empty-yielding Function-like one-to-one constant functional Function-yielding V36() finite finite-yielding V41() V42() V44( {} ) set

the empty ext-real non positive non negative epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural Relation-like non-empty empty-yielding Function-like one-to-one constant functional Function-yielding V36() finite finite-yielding V41() V42() V44( {} ) set is empty ext-real non positive non negative epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural Relation-like non-empty empty-yielding Function-like one-to-one constant functional Function-yielding V36() finite finite-yielding V41() V42() V44( {} ) set

1 is non empty ext-real epsilon-transitive epsilon-connected ordinal natural finite V42() Element of NAT

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

[:1,1:] is non empty Relation-like finite set

bool [:1,1:] is non empty finite V41() set

[:[:1,1:],1:] is non empty Relation-like finite set

bool [:[:1,1:],1:] is non empty finite V41() set

0 is empty ext-real non positive non negative epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural Relation-like non-empty empty-yielding Function-like one-to-one constant functional Function-yielding V36() finite finite-yielding V41() V42() V44( {} ) Element of NAT

{{}} is non empty trivial functional finite V41() V44(1) set

F

the carrier of F

bool the carrier of F

F

F

[:F

bool [:F

L is set

L is Element of F

L is Element of the carrier of F

l1 is Element of the carrier of F

Y is set

L is Relation-like Function-like set

dom L is set

rng L is set

L is Relation-like F

L is Element of the carrier of F

L . L is set

l1 is Element of F

Y is Element of the carrier of F

L is Element of the carrier of F

L . L is set

L is non empty V110() reflexive transitive antisymmetric with_suprema with_infima RelStr

the carrier of L is non empty set

bool the carrier of L is non empty set

L is non empty Element of bool the carrier of L

[:L,L:] is non empty Relation-like set

bool [:L,L:] is non empty set

L is Relation-like L -defined L -valued Function-like V32(L,L) Element of bool [:L,L:]

l1 is ext-real epsilon-transitive epsilon-connected ordinal natural finite V42() Element of NAT

iter (L,l1) is Relation-like set

L is non empty V110() reflexive transitive antisymmetric with_suprema with_infima RelStr

the carrier of L is non empty set

bool the carrier of L is non empty set

L is non empty Element of bool the carrier of L

L is non empty Element of bool the carrier of L

[:L,L:] is non empty Relation-like set

bool [:L,L:] is non empty set

l1 is Relation-like L -defined L -valued Function-like V32(L,L) Element of bool [:L,L:]

Y is Element of L

l1 . Y is set

l1 . Y is Element of L

L is non empty V110() reflexive transitive antisymmetric RelStr

the carrier of L is non empty set

bool the carrier of L is non empty set

L is strongly_connected Element of bool the carrier of L

the InternalRel of L is Relation-like the carrier of L -defined the carrier of L -valued V28( the carrier of L) reflexive antisymmetric transitive 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

L is Element of the carrier of L

l1 is Element of the carrier of L

[L,l1] is Element of [: the carrier of L, the carrier of L:]

{L,l1} is non empty finite set

{L} is non empty trivial finite V44(1) set

{{L,l1},{L}} is non empty finite V41() set

[l1,L] is Element of [: the carrier of L, the carrier of L:]

{l1,L} is non empty finite set

{l1} is non empty trivial finite V44(1) set

{{l1,L},{l1}} is non empty finite V41() set

L is Element of the carrier of L

l1 is Element of the carrier of L

[L,l1] is Element of [: the carrier of L, the carrier of L:]

{L,l1} is non empty finite set

{L} is non empty trivial finite V44(1) set

{{L,l1},{L}} is non empty finite V41() set

[l1,L] is Element of [: the carrier of L, the carrier of L:]

{l1,L} is non empty finite set

{l1} is non empty trivial finite V44(1) set

{{l1,L},{l1}} is non empty finite V41() set

the set is set

{ the set } is non empty trivial finite V44(1) set

[:{ the set },{ the set }:] is non empty Relation-like finite set

bool [:{ the set },{ the set }:] is non empty finite V41() set

the Relation-like { the set } -defined { the set } -valued V28({ the set }) finite reflexive antisymmetric transitive Element of bool [:{ the set },{ the set }:] is Relation-like { the set } -defined { the set } -valued V28({ the set }) finite reflexive antisymmetric transitive Element of bool [:{ the set },{ the set }:]

RelStr(# { the set }, the Relation-like { the set } -defined { the set } -valued V28({ the set }) finite reflexive antisymmetric transitive Element of bool [:{ the set },{ the set }:] #) is non empty trivial finite 1 -element strict V110() reflexive transitive antisymmetric lower-bounded upper-bounded V167() connected up-complete /\-complete distributive Heyting complemented Boolean with_suprema with_infima complete satisfying_MC meet-continuous satisfying_axiom_of_approximation continuous completely-distributive RelStr

L is non empty trivial finite 1 -element V110() reflexive transitive antisymmetric lower-bounded upper-bounded V167() connected up-complete /\-complete distributive Heyting complemented Boolean with_suprema with_infima complete satisfying_MC meet-continuous satisfying_axiom_of_approximation continuous completely-distributive RelStr

L is non empty V110() reflexive transitive antisymmetric with_infima RelStr

the carrier of L is non empty set

L is non empty V110() reflexive transitive antisymmetric with_infima RelStr

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

L is Relation-like the carrier of L -defined the carrier of L -valued Function-like V32( the carrier of L, the carrier of L) Element of bool [: the carrier of L, the carrier of L:]

dom L is Element of bool the carrier of L

bool the carrier of L is non empty set

l1 is Element of the carrier of L

Y is Element of the carrier of L

l1 "/\" Y is Element of the carrier of L

L . (l1 "/\" Y) is Element of the carrier of L

L . l1 is Element of the carrier of L

L . Y is Element of the carrier of L

(L . l1) "/\" (L . Y) is Element of the carrier of L

{l1,Y} is non empty finite Element of bool the carrier of L

L .: {l1,Y} is non empty finite Element of bool the carrier of L

bool the carrier of L is non empty set

{(L . l1),(L . Y)} is non empty finite Element of bool the carrier of L

"/\" ({l1,Y},L) is Element of the carrier of L

L . ("/\" ({l1,Y},L)) is Element of the carrier of L

"/\" ({(L . l1),(L . Y)},L) is Element of the carrier of L

l1 is Element of the carrier of L

Y is Element of the carrier of L

{l1,Y} is non empty finite Element of bool the carrier of L

L .: {l1,Y} is non empty finite Element of bool the carrier of L

bool the carrier of L is non empty set

L . l1 is Element of the carrier of L

L . Y is Element of the carrier of L

{(L . l1),(L . Y)} is non empty finite Element of bool the carrier of L

"/\" ((L .: {l1,Y}),L) is Element of the carrier of L

(L . l1) "/\" (L . Y) is Element of the carrier of L

l1 "/\" Y is Element of the carrier of L

L . (l1 "/\" Y) is Element of the carrier of L

"/\" ({l1,Y},L) is Element of the carrier of L

L . ("/\" ({l1,Y},L)) is Element of the carrier of L

L is non empty V110() reflexive transitive antisymmetric with_suprema RelStr

the carrier of L is non empty set

L is non empty V110() reflexive transitive antisymmetric with_suprema RelStr

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

L is Relation-like the carrier of L -defined the carrier of L -valued Function-like V32( the carrier of L, the carrier of L) Element of bool [: the carrier of L, the carrier of L:]

dom L is Element of bool the carrier of L

bool the carrier of L is non empty set

l1 is Element of the carrier of L

Y is Element of the carrier of L

l1 "\/" Y is Element of the carrier of L

L . (l1 "\/" Y) is Element of the carrier of L

L . l1 is Element of the carrier of L

L . Y is Element of the carrier of L

(L . l1) "\/" (L . Y) is Element of the carrier of L

{l1,Y} is non empty finite Element of bool the carrier of L

L .: {l1,Y} is non empty finite Element of bool the carrier of L

bool the carrier of L is non empty set

{(L . l1),(L . Y)} is non empty finite Element of bool the carrier of L

"\/" ({l1,Y},L) is Element of the carrier of L

L . ("\/" ({l1,Y},L)) is Element of the carrier of L

"\/" ({(L . l1),(L . Y)},L) is Element of the carrier of L

l1 is Element of the carrier of L

Y is Element of the carrier of L

{l1,Y} is non empty finite Element of bool the carrier of L

L .: {l1,Y} is non empty finite Element of bool the carrier of L

bool the carrier of L is non empty set

L . l1 is Element of the carrier of L

L . Y is Element of the carrier of L

{(L . l1),(L . Y)} is non empty finite Element of bool the carrier of L

"\/" ((L .: {l1,Y}),L) is Element of the carrier of L

(L . l1) "\/" (L . Y) is Element of the carrier of L

l1 "\/" Y is Element of the carrier of L

L . (l1 "\/" Y) is Element of the carrier of L

"\/" ({l1,Y},L) is Element of the carrier of L

L . ("\/" ({l1,Y},L)) is Element of the carrier of L

L is non empty V110() reflexive transitive antisymmetric with_suprema with_infima RelStr

the carrier of L is non empty set

L is non empty V110() reflexive transitive antisymmetric with_suprema with_infima RelStr

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

L is Relation-like the carrier of L -defined the carrier of L -valued Function-like V32( the carrier of L, the carrier of L) Element of bool [: the carrier of L, the carrier of L:]

l1 is Element of the carrier of L

Y is Element of the carrier of L

Y is Element of the carrier of L

Y "\/" Y is Element of the carrier of L

l1 "/\" (Y "\/" Y) is Element of the carrier of L

l1 "/\" Y is Element of the carrier of L

l1 "/\" Y is Element of the carrier of L

(l1 "/\" Y) "\/" (l1 "/\" Y) is Element of the carrier of L

Y "\/" Y is Element of the carrier of L

l1 "/\" (Y "\/" Y) is Element of the carrier of L

L . (l1 "/\" (Y "\/" Y)) is Element of the carrier of L

L . l1 is Element of the carrier of L

L . (Y "\/" Y) is Element of the carrier of L

(L . l1) "/\" (L . (Y "\/" Y)) is Element of the carrier of L

L . Y is Element of the carrier of L

L . Y is Element of the carrier of L

(L . Y) "\/" (L . Y) is Element of the carrier of L

(L . l1) "/\" ((L . Y) "\/" (L . Y)) is Element of the carrier of L

(L . l1) "/\" (L . Y) is Element of the carrier of L

(L . l1) "/\" (L . Y) is Element of the carrier of L

((L . l1) "/\" (L . Y)) "\/" ((L . l1) "/\" (L . Y)) is Element of the carrier of L

l1 "/\" Y is Element of the carrier of L

L . (l1 "/\" Y) is Element of the carrier of L

((L . l1) "/\" (L . Y)) "\/" (L . (l1 "/\" Y)) is Element of the carrier of L

l1 "/\" Y is Element of the carrier of L

L . (l1 "/\" Y) is Element of the carrier of L

(L . (l1 "/\" Y)) "\/" (L . (l1 "/\" Y)) is Element of the carrier of L

(l1 "/\" Y) "\/" (l1 "/\" Y) is Element of the carrier of L

L . ((l1 "/\" Y) "\/" (l1 "/\" Y)) is Element of the carrier of L

L is non empty V110() reflexive transitive antisymmetric lower-bounded upper-bounded V167() up-complete /\-complete with_suprema with_infima complete RelStr

the carrier of L is non empty set

L is non empty V110() reflexive transitive antisymmetric lower-bounded upper-bounded V167() up-complete /\-complete with_suprema with_infima complete RelStr

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

Bottom L is Element of the carrier of L

L --> (Bottom L) is Relation-like the carrier of L -defined the carrier of L -valued Function-like V32( the carrier of L, the carrier of L) Element of bool [: the carrier of L, the carrier of L:]

the carrier of L --> (Bottom L) is non empty Relation-like the carrier of L -defined the carrier of L -valued Function-like constant V28( the carrier of L) V32( the carrier of L, the carrier of L) Element of bool [: the carrier of L, the carrier of L:]

bool the carrier of L is non empty set

Y is Element of bool the carrier of L

(L --> (Bottom L)) .: Y is Element of bool the carrier of L

bool the carrier of L is non empty set

"\/" (((L --> (Bottom L)) .: Y),L) is Element of the carrier of L

"\/" (Y,L) is Element of the carrier of L

(L --> (Bottom L)) . ("\/" (Y,L)) is Element of the carrier of L

rng (L --> (Bottom L)) is Element of bool the carrier of L

{(Bottom L)} is non empty trivial finite V44(1) Element of bool the carrier of L

Y is non empty Element of bool the carrier of L

the Element of Y is Element of Y

(L --> (Bottom L)) . the Element of Y is Element of the carrier of L

L is non empty V110() reflexive transitive antisymmetric with_suprema RelStr

the carrier of L is non empty set

L is non empty V110() reflexive transitive antisymmetric with_suprema RelStr

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

L is Relation-like the carrier of L -defined the carrier of L -valued Function-like V32( the carrier of L, the carrier of L) Element of bool [: the carrier of L, the carrier of L:]

l1 is Element of the carrier of L

Y is Element of the carrier of L

L . l1 is set

L . Y is set

Y "\/" l1 is Element of the carrier of L

{l1,Y} is non empty finite Element of bool the carrier of L

bool the carrier of L is non empty set

Y is Element of the carrier of L

x is Element of the carrier of L

dom L is Element of bool the carrier of L

Y is Element of the carrier of L

L .: {l1,Y} is non empty finite Element of bool the carrier of L

bool the carrier of L is non empty set

"\/" ((L .: {l1,Y}),L) is Element of the carrier of L

"\/" ({l1,Y},L) is Element of the carrier of L

L . ("\/" ({l1,Y},L)) is Element of the carrier of L

L . Y is Element of the carrier of L

L . l1 is Element of the carrier of L

{(L . l1),(L . Y)} is non empty finite Element of bool the carrier of L

"\/" ({(L . l1),(L . Y)},L) is Element of the carrier of L

(L . Y) "\/" (L . l1) is Element of the carrier of L

Y is Element of the carrier of L

x is Element of the carrier of L

L is non empty V110() reflexive transitive antisymmetric lower-bounded upper-bounded V167() up-complete /\-complete with_suprema with_infima complete RelStr

the carrier of L is non empty set

L is non empty V110() reflexive transitive antisymmetric lower-bounded upper-bounded V167() up-complete /\-complete with_suprema with_infima complete RelStr

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

L is Relation-like the carrier of L -defined the carrier of L -valued Function-like V32( the carrier of L, the carrier of L) sups-preserving join-preserving directed-sups-preserving Element of bool [: the carrier of L, the carrier of L:]

bool the carrier of L is non empty set

l1 is Element of the carrier of L

{l1} is non empty trivial finite V44(1) Element of bool the carrier of L

Y is non empty directed Element of bool the carrier of L

"\/" (Y,L) is Element of the carrier of L

l1 "/\" ("\/" (Y,L)) is Element of the carrier of L

{l1} "/\" Y is non empty Element of bool the carrier of L

"\/" (({l1} "/\" Y),L) is Element of the carrier of L

Y is non empty directed Element of bool the carrier of L

Y "/\" Y is non empty directed Element of bool the carrier of L

{l1} "/\" Y is non empty Element of bool the carrier of L

bool the carrier of L is non empty set

L .: Y is non empty Element of bool the carrier of L

dom L is Element of bool the carrier of L

L . l1 is Element of the carrier of L

{(L . l1)} is non empty trivial finite V44(1) Element of bool the carrier of L

{(L . l1)} "/\" (L .: Y) is non empty Element of bool the carrier of L

{ ((L . l1) "/\" b

L .: ({l1} "/\" Y) is non empty Element of bool the carrier of L

p is set

f1 is Element of the carrier of L

(L . l1) "/\" f1 is Element of the carrier of L

D is set

L . D is set

f is Element of the carrier of L

l1 "/\" f is Element of the carrier of L

{ (l1 "/\" b

{l1,f} is non empty finite Element of bool the carrier of L

L . (l1 "/\" f) is Element of the carrier of L

{ (l1 "/\" b

p is set

f1 is set

L . f1 is set

D is Element of the carrier of L

f is Element of the carrier of L

l1 "/\" f is Element of the carrier of L

L . f is Element of the carrier of L

{l1,f} is non empty finite Element of bool the carrier of L

P is Element of the carrier of L

(L . l1) "/\" P is Element of the carrier of L

l1 "/\" ("\/" (Y,L)) is Element of the carrier of L

L . (l1 "/\" ("\/" (Y,L))) is Element of the carrier of L

L . ("\/" (Y,L)) is Element of the carrier of L

(L . l1) "/\" (L . ("\/" (Y,L))) is Element of the carrier of L

x is directed Element of bool the carrier of L

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

(L . l1) "/\" ("\/" (x,L)) is Element of the carrier of L

{(L . l1)} "/\" x is Element of bool the carrier of L

"\/" (({(L . l1)} "/\" x),L) is Element of the carrier of L

"\/" ((L .: ({l1} "/\" Y)),L) is Element of the carrier of L

"\/" (({l1} "/\" Y),L) is Element of the carrier of L

L . ("\/" (({l1} "/\" Y),L)) is Element of the carrier of L

L is non empty V110() reflexive RelStr

the carrier of L is non empty set

bool the carrier of L is non empty set

L is non empty V110() reflexive transitive antisymmetric upper-bounded up-complete with_suprema with_infima RelStr

the carrier of L is non empty set

bool the carrier of L is non empty set

L is upper Element of bool the carrier of L

L is Element of the carrier of L

waybelow L is directed lower Element of bool the carrier of L

l1 is Element of the carrier of L

{ b

L is Element of the carrier of L

waybelow L is directed lower Element of bool the carrier of L

l1 is set

{ b

Y is Element of the carrier of L

L is non empty V110() reflexive transitive antisymmetric upper-bounded up-complete with_suprema with_infima RelStr

the carrier of L is non empty set

bool the carrier of L is non empty set

L is upper Element of bool the carrier of L

{ (wayabove b

union { (wayabove b

L is set

l1 is Element of L

Y is Element of the carrier of L

Y is Element of the carrier of L

{ b

wayabove Y is upper Element of bool the carrier of L

L is set

l1 is set

Y is Element of the carrier of L

wayabove Y is upper Element of bool the carrier of L

{ b

Y is Element of the carrier of L

L is Element of the carrier of L

l1 is set

Y is Element of the carrier of L

wayabove Y is upper Element of bool the carrier of L

{ b

Y is Element of the carrier of L

L is non empty V110() reflexive transitive antisymmetric lower-bounded upper-bounded V167() up-complete /\-complete with_suprema with_infima complete RelStr

the carrier of L is non empty set

bool the carrier of L is non empty set

[#] L is non empty non proper directed filtered lower upper Element of bool the carrier of L

L is Element of the carrier of L

Bottom L is Element of the carrier of L

L is non empty V110() reflexive transitive antisymmetric lower-bounded upper-bounded V167() up-complete /\-complete with_suprema with_infima complete satisfying_axiom_of_approximation continuous RelStr

the carrier of L is non empty set

L is Element of the carrier of L

wayabove L is upper Element of bool the carrier of L

bool the carrier of L is non empty set

L is Element of the carrier of L

l1 is Element of the carrier of L

L is non empty V110() reflexive transitive antisymmetric lower-bounded upper-bounded V167() up-complete /\-complete with_suprema with_infima complete satisfying_axiom_of_approximation continuous RelStr

the carrier of L is non empty set

bool the carrier of L is non empty set

L is Element of the carrier of L

L is Element of the carrier of L

wayabove L is upper Element of bool the carrier of L

l1 is non empty Element of bool the carrier of L

Y is Element of the carrier of L

Y is Element of the carrier of L

[:l1,l1:] is non empty Relation-like set

bool [:l1,l1:] is non empty set

Y is Relation-like l1 -defined l1 -valued Function-like V32(l1,l1) Element of bool [:l1,l1:]

{ (uparrow b

x is set

p is Element of the carrier of L

uparrow p is non empty filtered upper Element of bool the carrier of L

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

uparrow {p} is non empty upper Element of bool the carrier of L

f1 is ext-real epsilon-transitive epsilon-connected ordinal natural finite V42() Element of NAT

(L,l1,Y,f1) is Relation-like l1 -defined l1 -valued Function-like V32(l1,l1) Element of bool [:l1,l1:]

(L,l1,Y,f1) . L is set

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

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

f1 is Element of bool the carrier of L

D is Element of bool the carrier of L

f1 \/ D is Element of bool the carrier of L

f is Element of the carrier of L

uparrow f is non empty filtered upper Element of bool the carrier of L

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

uparrow {f} is non empty upper Element of bool the carrier of L

P is ext-real epsilon-transitive epsilon-connected ordinal natural finite V42() Element of NAT

(L,l1,Y,P) is Relation-like l1 -defined l1 -valued Function-like V32(l1,l1) Element of bool [:l1,l1:]

(L,l1,Y,P) . L is set

P is ext-real epsilon-transitive epsilon-connected ordinal natural finite V42() Element of NAT

(L,l1,Y,P) is Relation-like l1 -defined l1 -valued Function-like V32(l1,l1) Element of bool [:l1,l1:]

(L,l1,Y,P) . L is set

R is Element of the carrier of L

uparrow R is non empty filtered upper Element of bool the carrier of L

{R} is non empty trivial finite V44(1) Element of bool the carrier of L

uparrow {R} is non empty upper Element of bool the carrier of L

R "/\" f is Element of the carrier of L

k1 is ext-real epsilon-transitive epsilon-connected ordinal natural finite V42() Element of NAT

(L,l1,Y,k1) is Relation-like l1 -defined l1 -valued Function-like V32(l1,l1) Element of bool [:l1,l1:]

(L,l1,Y,k1) . L is set

k1 is ext-real epsilon-transitive epsilon-connected ordinal natural finite V42() Element of NAT

(L,l1,Y,k1) is Relation-like l1 -defined l1 -valued Function-like V32(l1,l1) Element of bool [:l1,l1:]

(L,l1,Y,k1) . L is set

p is Element of l1

a is ext-real epsilon-transitive epsilon-connected ordinal natural finite V42() Element of NAT

(L,l1,Y,a) is Relation-like l1 -defined l1 -valued Function-like V32(l1,l1) Element of bool [:l1,l1:]

(L,l1,l1,(L,l1,Y,a),p) is Element of the carrier of L

b is ext-real epsilon-transitive epsilon-connected ordinal natural finite V42() Element of NAT

a + b is ext-real epsilon-transitive epsilon-connected ordinal natural finite V42() Element of NAT

(L,l1,Y,(a + b)) is Relation-like l1 -defined l1 -valued Function-like V32(l1,l1) Element of bool [:l1,l1:]

(L,l1,l1,(L,l1,Y,(a + b)),p) is Element of the carrier of L

b + 1 is ext-real epsilon-transitive epsilon-connected ordinal natural finite V42() Element of NAT

a + (b + 1) is ext-real epsilon-transitive epsilon-connected ordinal natural finite V42() Element of NAT

(L,l1,Y,(a + (b + 1))) is Relation-like l1 -defined l1 -valued Function-like V32(l1,l1) Element of bool [:l1,l1:]

(L,l1,l1,(L,l1,Y,(a + (b + 1))),p) is Element of the carrier of L

Y . (L,l1,l1,(L,l1,Y,(a + b)),p) is set

znk is Element of the carrier of L

dom (L,l1,Y,(a + b)) is Element of bool l1

bool l1 is non empty set

Y * (L,l1,Y,(a + b)) is Relation-like l1 -defined l1 -valued Function-like Element of bool [:l1,l1:]

(Y * (L,l1,Y,(a + b))) . p is set

(a + b) + 1 is ext-real epsilon-transitive epsilon-connected ordinal natural finite V42() Element of NAT

(L,l1,Y,((a + b) + 1)) is Relation-like l1 -defined l1 -valued Function-like V32(l1,l1) Element of bool [:l1,l1:]

(L,l1,l1,(L,l1,Y,((a + b) + 1)),p) is Element of the carrier of L

a + 0 is ext-real epsilon-transitive epsilon-connected ordinal natural finite V42() Element of NAT

(L,l1,Y,(a + 0)) is Relation-like l1 -defined l1 -valued Function-like V32(l1,l1) Element of bool [:l1,l1:]

(L,l1,l1,(L,l1,Y,(a + 0)),p) is Element of the carrier of L

b is ext-real epsilon-transitive epsilon-connected ordinal natural finite V42() Element of NAT

a + b is ext-real epsilon-transitive epsilon-connected ordinal natural finite V42() Element of NAT

(L,l1,Y,(a + b)) is Relation-like l1 -defined l1 -valued Function-like V32(l1,l1) Element of bool [:l1,l1:]

(L,l1,l1,(L,l1,Y,(a + b)),p) is Element of the carrier of L

a is ext-real epsilon-transitive epsilon-connected ordinal natural finite V42() set

k1 + a is ext-real epsilon-transitive epsilon-connected ordinal natural finite V42() Element of NAT

uparrow (R "/\" f) is non empty filtered upper Element of bool the carrier of L

{(R "/\" f)} is non empty trivial finite V44(1) Element of bool the carrier of L

uparrow {(R "/\" f)} is non empty upper Element of bool the carrier of L

a is ext-real epsilon-transitive epsilon-connected ordinal natural finite V42() set

P + a is ext-real epsilon-transitive epsilon-connected ordinal natural finite V42() Element of NAT

uparrow (R "/\" f) is non empty filtered upper Element of bool the carrier of L

{(R "/\" f)} is non empty trivial finite V44(1) Element of bool the carrier of L

uparrow {(R "/\" f)} is non empty upper Element of bool the carrier of L

uparrow (R "/\" f) is non empty filtered upper Element of bool the carrier of L

{(R "/\" f)} is non empty trivial finite V44(1) Element of bool the carrier of L

uparrow {(R "/\" f)} is non empty upper Element of bool the carrier of L

uparrow (R "/\" f) is non empty filtered upper Element of bool the carrier of L

{(R "/\" f)} is non empty trivial finite V44(1) Element of bool the carrier of L

uparrow {(R "/\" f)} is non empty upper Element of bool the carrier of L

p is Element of bool the carrier of L

f1 is Element of the carrier of L

uparrow f1 is non empty filtered upper Element of bool the carrier of L

{f1} is non empty trivial finite V44(1) Element of bool the carrier of L

uparrow {f1} is non empty upper Element of bool the carrier of L

D is ext-real epsilon-transitive epsilon-connected ordinal natural finite V42() Element of NAT

(L,l1,Y,D) is Relation-like l1 -defined l1 -valued Function-like V32(l1,l1) Element of bool [:l1,l1:]

(L,l1,Y,D) . L is set

uparrow L is non empty filtered upper Element of bool the carrier of L

{L} is non empty trivial finite V44(1) Element of bool the carrier of L

uparrow {L} is non empty upper Element of bool the carrier of L

union { (uparrow b

f1 is set

D is set

f is Element of the carrier of L

uparrow f is non empty filtered upper Element of bool the carrier of L

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

uparrow {f} is non empty upper Element of bool the carrier of L

P is Element of bool the carrier of L

{ b

( b

R is Element of the carrier of L

f2 is Element of the carrier of L

D is Element of the carrier of L

f1 is Element of bool the carrier of L

f is set

P is Element of the carrier of L

uparrow P is non empty filtered upper Element of bool the carrier of L

{P} is non empty trivial finite V44(1) Element of bool the carrier of L

uparrow {P} is non empty upper Element of bool the carrier of L

R is ext-real epsilon-transitive epsilon-connected ordinal natural finite V42() Element of NAT

(L,l1,Y,R) is Relation-like l1 -defined l1 -valued Function-like V32(l1,l1) Element of bool [:l1,l1:]

(L,l1,Y,R) . L is set

R is ext-real epsilon-transitive epsilon-connected ordinal natural finite V42() Element of NAT

(L,l1,Y,R) is Relation-like l1 -defined l1 -valued Function-like V32(l1,l1) Element of bool [:l1,l1:]

(L,l1,Y,R) . L is set

Y . P is set

f2 is Element of the carrier of L

uparrow f2 is non empty filtered upper Element of bool the carrier of L

{f2} is non empty trivial finite V44(1) Element of bool the carrier of L

uparrow {f2} is non empty upper Element of bool the carrier of L

dom (L,l1,Y,R) is Element of bool l1

bool l1 is non empty set

Y * (L,l1,Y,R) is Relation-like l1 -defined l1 -valued Function-like Element of bool [:l1,l1:]

(Y * (L,l1,Y,R)) . L is set

R + 1 is ext-real epsilon-transitive epsilon-connected ordinal natural finite V42() Element of NAT

(L,l1,Y,(R + 1)) is Relation-like l1 -defined l1 -valued Function-like V32(l1,l1) Element of bool [:l1,l1:]

(L,l1,Y,(R + 1)) . L is set

k1 is Element of bool the carrier of L

{ b

( b

a is Element of the carrier of L

b is Element of the carrier of L

b is Element of the carrier of L

dom Y is Element of bool l1

field Y is set

dom Y is set

rng Y is set

(dom Y) \/ (rng Y) is set

(L,l1,Y,0) is Relation-like l1 -defined l1 -valued Function-like V32(l1,l1) Element of bool [:l1,l1:]

(L,l1,Y,0) . L is set

id (field Y) is Relation-like field Y -defined field Y -valued Function-like one-to-one V28( field Y) Element of bool [:(field Y),(field Y):]

[:(field Y),(field Y):] is Relation-like set

bool [:(field Y),(field Y):] is non empty set

(id (field Y)) . L is set

D is Element of bool the carrier of L

f is Element of the carrier of L

uparrow f is non empty filtered upper Element of bool the carrier of L

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

uparrow {f} is non empty upper Element of bool the carrier of L

P is ext-real epsilon-transitive epsilon-connected ordinal natural finite V42() Element of NAT

(L,l1,Y,P) is Relation-like l1 -defined l1 -valued Function-like V32(l1,l1) Element of bool [:l1,l1:]

(L,l1,Y,P) . L is set

D is non empty filtered upper (L) Element of bool the carrier of L

f is set

P is set

f2 is Element of the carrier of L

uparrow f2 is non empty filtered upper Element of bool the carrier of L

{f2} is non empty trivial finite V44(1) Element of bool the carrier of L

uparrow {f2} is non empty upper Element of bool the carrier of L

k1 is ext-real epsilon-transitive epsilon-connected ordinal natural finite V42() Element of NAT

(L,l1,Y,k1) is Relation-like l1 -defined l1 -valued Function-like V32(l1,l1) Element of bool [:l1,l1:]

(L,l1,Y,k1) . L is set

R is Element of the carrier of L

L is non empty V110() reflexive transitive antisymmetric lower-bounded upper-bounded V167() up-complete /\-complete with_suprema with_infima complete RelStr

the carrier of L is non empty set

bool the carrier of L is non empty set

L is upper (L) Element of bool the carrier of L

L ` is Element of bool the carrier of L

the carrier of L \ L is set

L is Element of the carrier of L

{ b

{L} is non empty trivial finite V44(1) Element of bool the carrier of L

Y is set

union Y is set

x is set

p is strongly_connected directed filtered Element of bool the carrier of L

the InternalRel of L is Relation-like the carrier of L -defined the carrier of L -valued V28( the carrier of L) reflexive antisymmetric transitive 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

x is Element of bool the carrier of L

p is set

f1 is set

[p,f1] is set

{p,f1} is non empty finite set

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

{{p,f1},{p}} is non empty finite V41() set

[f1,p] is set

{f1,p} is non empty finite set

{f1} is non empty trivial finite V44(1) set

{{f1,p},{f1}} is non empty finite V41() set

D is set

f is set

R is strongly_connected directed filtered Element of bool the carrier of L

f2 is strongly_connected directed filtered Element of bool the carrier of L

R is strongly_connected directed filtered Element of bool the carrier of L

P is strongly_connected directed filtered Element of bool the carrier of L

f1 is set

D is strongly_connected directed filtered Element of bool the carrier of L

the Element of Y is Element of Y

p is strongly_connected directed filtered Element of bool the carrier of L

D is strongly_connected directed filtered Element of bool the carrier of L

Y is strongly_connected directed filtered Element of bool the carrier of L

Y is set

x is strongly_connected directed filtered Element of bool the carrier of L

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

f1 is Element of the carrier of L

{f1} is non empty trivial finite V44(1) Element of bool the carrier of L

x \/ {f1} is non empty Element of bool the carrier of L

the InternalRel of L is Relation-like the carrier of L -defined the carrier of L -valued V28( the carrier of L) reflexive antisymmetric transitive 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

f is set

P is set

[f,P] is set

{f,P} is non empty finite set

{f} is non empty trivial finite V44(1) set

{{f,P},{f}} is non empty finite V41() set

[P,f] is set

{P,f} is non empty finite set

{P} is non empty trivial finite V44(1) set

{{P,f},{P}} is non empty finite V41() set

f2 is Element of the carrier of L

R is Element of the carrier of L

f2 is Element of the carrier of L

R is Element of the carrier of L

R is Element of the carrier of L

f is strongly_connected directed filtered Element of bool the carrier of L

f1 is Element of the carrier of L

D is Element of the carrier of L

L is non empty RelStr

the carrier of L is non empty set

L is non empty RelStr

the carrier of L is non empty set

L is non empty RelStr

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

L is Element of the carrier of L

l1 is Element of the carrier of L

L is Element of bool the carrier of L

L is Element of bool the carrier of L

l1 is set

Y is Element of the carrier of L

l1 is set

Y is Element of the carrier of L

L is non empty antisymmetric upper-bounded with_infima RelStr

Top L is Element of the carrier of L

the carrier of L is non empty set

L is Element of the carrier of L

L is Element of the carrier of L

L "/\" L is Element of the carrier of L

L "/\" L is Element of the carrier of L

L is non empty antisymmetric upper-bounded with_infima RelStr

the carrier of L is non empty set

Top L is Element of the carrier of L

L is non empty V110() reflexive transitive antisymmetric with_infima RelStr

the carrier of L is non empty set

bool the carrier of L is non empty set

L is Element of the carrier of L

L is non empty finite Element of bool the carrier of L

"/\" (L,L) is Element of the carrier of L

l1 is set

Y is set

"/\" (Y,L) is Element of the carrier of L

{l1} is non empty trivial finite V44(1) set

Y \/ {l1} is non empty set

"/\" ((Y \/ {l1}),L) is Element of the carrier of L

Y is Element of the carrier of L

{Y} is non empty trivial finite V44(1) Element of bool the carrier of L

Y \/ {Y} is non empty set

"/\" ((Y \/ {Y}),L) is Element of the carrier of L

Y is Element of the carrier of L

{Y} is non empty trivial finite V44(1) Element of bool the carrier of L

"/\" ({Y},L) is Element of the carrier of L

x is finite Element of bool the carrier of L

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

("/\" (x,L)) "/\" ("/\" ({Y},L)) is Element of the carrier of L

"/\" ({},L) is Element of the carrier of L

L is Element of the carrier of L

l1 is Element of the carrier of L

L "/\" l1 is Element of the carrier of L

L "/\" l1 is Element of the carrier of L

{L,l1} is non empty finite Element of bool the carrier of L

"/\" ({L,l1},L) is Element of the carrier of L

L is non empty V110() reflexive transitive antisymmetric with_suprema with_infima RelStr

the carrier of L is non empty set

bool the carrier of L is non empty set

L is Element of the carrier of L

uparrow L is non empty filtered upper Element of bool the carrier of L

{L} is non empty trivial finite V44(1) Element of bool the carrier of L

uparrow {L} is non empty upper Element of bool the carrier of L

(uparrow L) \ {L} is Element of bool the carrier of L

l1 is Element of the carrier of L

Y is Element of the carrier of L

l1 "/\" Y is Element of the carrier of L

Y is Element of the carrier of L

L is non empty V110() reflexive transitive antisymmetric with_suprema with_infima RelStr

the carrier of L is non empty set

bool the carrier of L is non empty set

L is Element of the carrier of L

L is non empty filtered upper Element of bool the carrier of L

L ` is Element of bool the carrier of L

the carrier of L \ L is set

the carrier of L \ L is Element of bool the carrier of L

Y is Element of the carrier of L

Y is Element of the carrier of L

Y "/\" Y is Element of the carrier of L

x is Element of the carrier of L

L is non empty V110() reflexive transitive antisymmetric lower-bounded upper-bounded V167() up-complete /\-complete with_suprema with_infima complete satisfying_axiom_of_approximation continuous RelStr

the carrier of L is non empty set

L is Element of the carrier of L

L is Element of the carrier of L

l1 is Element of the carrier of L

waybelow l1 is non empty directed lower Element of bool the carrier of L

bool the carrier of L is non empty set

Y is Element of the carrier of L

waybelow Y is non empty directed lower Element of bool the carrier of L

l1 is Element of the carrier of L

bool the carrier of L is non empty set

wayabove l1 is upper Element of bool the carrier of L

Y is non empty filtered upper (L) Element of bool the carrier of L

uparrow l1 is non empty filtered upper Element of bool the carrier of L

{l1} is non empty trivial finite V44(1) Element of bool the carrier of L

uparrow {l1} is non empty upper Element of bool the carrier of L

the carrier of L \ Y is Element of bool the carrier of L

Y ` is Element of bool the carrier of L

the carrier of L \ Y is set

Y 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

L is non empty V110() reflexive transitive antisymmetric lower-bounded upper-bounded V167() up-complete /\-complete with_suprema with_infima complete RelStr

the carrier of L is non empty set

bool the carrier of L is non empty set

L is Element of bool the carrier of L

bool L is non empty set

L is Element of the carrier of L

uparrow L is non empty filtered upper Element of bool the carrier of L

{L} is non empty trivial finite V44(1) Element of bool the carrier of L

uparrow {L} is non empty upper Element of bool the carrier of L

(uparrow L) /\ L is Element of bool the carrier of L

l1 is set

l1 is Element of bool L

"/\" (l1,L) is Element of the carrier of L

L is Element of the carrier of L

uparrow L is non empty filtered upper Element of bool the carrier of L

{L} is non empty trivial finite V44(1) Element of bool the carrier of L

uparrow {L} is non empty upper Element of bool the carrier of L

(uparrow L) /\ L is Element of bool the carrier of L

"/\" (((uparrow L) /\ L),L) is Element of the carrier of L

l1 is Element of bool L

"/\" (l1,L) is Element of the carrier of L

Y is Element of the carrier of L

x is Element of the carrier of L

Y is Element of the carrier of L

L is non empty V110() reflexive transitive antisymmetric lower-bounded upper-bounded V167() up-complete /\-complete with_suprema with_infima complete RelStr

the carrier of L is non empty set

bool the carrier of L is non empty set

L is Element of bool the carrier of L

L is Element of bool the carrier of L

bool L is non empty set

l1 is set

Y is Element of the carrier of L

uparrow Y is non empty filtered upper Element of bool the carrier of L

{Y} is non empty trivial finite V44(1) Element of bool the carrier of L

uparrow {Y} is non empty upper Element of bool the carrier of L

(uparrow Y) /\ L is Element of bool the carrier of L

(uparrow Y) /\ L is Element of bool the carrier of L

"/\" (((uparrow Y) /\ L),L) is Element of the carrier of L

{ ("/\" (b

l1 is set

Y is Element of bool the carrier of L

"/\" (Y,L) is Element of the carrier of L

Y is set

Y is Element of the carrier of L

{Y} is non empty trivial finite V44(1) Element of bool the carrier of L

x is Element of bool the carrier of L

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

l1 is Element of bool the carrier of L

bool L is non empty set

Y is Element of the carrier of L

bool l1 is non empty set

Y is Element of bool l1

"/\" (Y,L) is Element of the carrier of L

{ b

union { b

p is set

f1 is set

D is Element of bool the carrier of L

"/\" (D,L) is Element of the carrier of L

{ ("/\" (b

D is set

f is Element of bool the carrier of L

"/\" (f,L) is Element of the carrier of L

D is set

f is Element of bool the carrier of L

"/\" (f,L) is Element of the carrier of L

p is Element of bool the carrier of L

D is set

f is Element of bool the carrier of L

"/\" (f,L) is Element of the carrier of L

"/\" ( { ("/\" (b

{ b

union { b

"/\" ((union { b

Y is Element of bool the carrier of L

"/\" (Y,L) is Element of the carrier of L

L is non empty V110() reflexive transitive antisymmetric lower-bounded upper-bounded V167() up-complete /\-complete with_suprema with_infima complete RelStr

the carrier of L is non empty set

bool the carrier of L is non empty set

L is Element of bool the carrier of L

l1 is Element of the carrier of L

L is Element of the carrier of L

bool L is non empty set

Y is Element of bool L

"/\" (Y,L) is Element of the carrier of L

Y is Element of the carrier of L

Y is Element of the carrier of L

L is Element of the carrier of L

uparrow L is non empty filtered upper Element of bool the carrier of L

{L} is non empty trivial finite V44(1) Element of bool the carrier of L

uparrow {L} is non empty upper Element of bool the carrier of L

(uparrow L) /\ L is Element of bool the carrier of L

"/\" (((uparrow L) /\ L),L) is Element of the carrier of L

Y is Element of the carrier of L

Y is Element of the carrier of L

L is non empty V110() reflexive transitive antisymmetric lower-bounded upper-bounded V167() up-complete /\-complete with_suprema with_infima complete satisfying_axiom_of_approximation continuous RelStr

the carrier of L is non empty set

bool the carrier of L is non empty set

(L) is Element of bool the carrier of L

Top L is Element of the carrier of L

{(Top L)} is non empty trivial finite V44(1) Element of bool the carrier of L

(L) \ {(Top L)} is Element of bool the carrier of L

L is Element of bool the carrier of L

l1 is Element of the carrier of L

L is Element of the carrier of L

Y is Element of the carrier of L

L is non empty V110() reflexive transitive antisymmetric lower-bounded upper-bounded V167() up-complete /\-complete with_suprema with_infima complete satisfying_axiom_of_approximation continuous RelStr

the carrier of L is non empty set

bool the carrier of L is non empty set

L is Element of bool the carrier of L

L is Element of bool the carrier of L

l1 is Element of the carrier of L

uparrow l1 is non empty filtered upper Element of bool the carrier of L

{l1} is non empty trivial finite V44(1) Element of bool the carrier of L

uparrow {l1} is non empty upper Element of bool the carrier of L

(uparrow l1) /\ L is Element of bool the carrier of L

"/\" (((uparrow l1) /\ L),L) is Element of the carrier of L

"/\" ((uparrow l1),L) is Element of the carrier of L

(uparrow l1) /\ L is Element of bool the carrier of L

"/\" (((uparrow l1) /\ L),L) is Element of the carrier of L

L is non empty RelStr

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

L is Element of the carrier of L

l1 is Element of the carrier of L

L is Element of bool the carrier of L

L is Element of bool the carrier of L

l1 is set

Y is Element of the carrier of L

l1 is set

Y is Element of the carrier of L

L is non empty RelStr

the carrier of L is non empty set

L is non empty antisymmetric upper-bounded RelStr

Top L is Element of the carrier of L

the carrier of L is non empty set

L is Element of the carrier of L

L is Element of the carrier of L

L "/\" L is Element of the carrier of L

L is non empty antisymmetric lower-bounded RelStr

Bottom L is Element of the carrier of L

the carrier of L is non empty set

L ~ is non empty strict antisymmetric upper-bounded RelStr

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 non empty strict RelStr

Top (L ~) is Element of the carrier of (L ~)

the carrier of (L ~) is non empty set

(Bottom L) ~ is Element of the carrier of (L ~)

L is non empty antisymmetric upper-bounded RelStr

the carrier of L is non empty set

Top L is Element of the carrier of L

L is non empty V110() reflexive transitive antisymmetric with_infima RelStr

the carrier of L is non empty set

bool the carrier of L is non empty set

L is Element of the carrier of L

L is non empty finite Element of bool the carrier of L

"/\" (L,L) is Element of the carrier of L

l1 is set

Y is set

"/\" (Y,L) is Element of the carrier of L

{l1} is non empty trivial finite V44(1) set

Y \/ {l1} is non empty set

"/\" ((Y \/ {l1}),L) is Element of the carrier of L

Y is Element of the carrier of L

{Y} is non empty trivial finite V44(1) Element of bool the carrier of L

Y \/ {Y} is non empty set

"/\" ((Y \/ {Y}),L) is Element of the carrier of L

Y is Element of the carrier of L

{Y} is non empty trivial finite V44(1) Element of bool the carrier of L

"/\" ({Y},L) is Element of the carrier of L

x is finite Element of bool the carrier of L

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

("/\" (x,L)) "/\" ("/\" ({Y},L)) is Element of the carrier of L

p is Element of the carrier of L

p is Element of the carrier of L

"/\" ({},L) is Element of the carrier of L

l1 is Element of the carrier of L

L is Element of the carrier of L

l1 is Element of the carrier of L

L "/\" l1 is Element of the carrier of L

{L,l1} is non empty finite Element of bool the carrier of L

"/\" ({L,l1},L) is Element of the carrier of L

L "/\" l1 is Element of the carrier of L

Y is Element of the carrier of L

L is non empty V110() reflexive transitive antisymmetric with_suprema RelStr

the carrier of L is non empty set

bool the carrier of L is non empty set

L is Element of the carrier of L

L ~ is non empty strict V110() reflexive transitive antisymmetric with_infima RelStr

the InternalRel of L is Relation-like the carrier of L -defined the carrier of L -valued V28( the carrier of L) reflexive antisymmetric transitive 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 non empty strict RelStr

L ~ is Element of the carrier of (L ~)

the carrier of (L ~) is non empty set

L is non empty finite Element of bool the carrier of L

"\/" (L,L) is Element of the carrier of L

bool the carrier of (L ~) is non empty set

("\/" (L,L)) ~ is Element of the carrier of (L ~)

Y is Element of the carrier of (L ~)

~ Y is Element of the carrier of L

l1 is non empty finite Element of bool the carrier of (L ~)

"/\" (l1,(L ~)) is Element of the carrier of (L ~)

Y is Element of the carrier of (L ~)

~ Y is Element of the carrier of L

L ~ is non empty strict V110() reflexive transitive antisymmetric with_infima RelStr

the InternalRel of L is Relation-like the carrier of L -defined the carrier of L -valued V28( the carrier of L) reflexive antisymmetric transitive 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 non empty strict RelStr

the carrier of (L ~) is non empty set

L is Element of the carrier of (L ~)

~ L is Element of the carrier of L

l1 is Element of the carrier of (L ~)

~ l1 is Element of the carrier of L

{(~ L),(~ l1)} is non empty finite Element of bool the carrier of L

L "/\" l1 is Element of the carrier of (L ~)

L ~ is Element of the carrier of (L ~)

~ (L "/\" l1) is Element of the carrier of L

"\/" ({(~ L),(~ l1)},L) is Element of the carrier of L

(~ L) "\/" (~ l1) is Element of the carrier of L

Y is Element of the carrier of L

L is non empty V110() reflexive transitive antisymmetric with_suprema with_infima RelStr

the carrier of L is non empty set

L is Element of the carrier of L

L is Element of the carrier of L

l1 is Element of the carrier of L

L "/\" l1 is Element of the carrier of L

L "/\" l1 is Element of the carrier of L

L is non empty V110() reflexive transitive antisymmetric with_suprema with_infima RelStr

the carrier of L is non empty set

L is Element of the carrier of L

L is set

{L} is non empty trivial finite V44(1) set

BoolePoset {L} is non empty strict V110() reflexive transitive antisymmetric lower-bounded upper-bounded V167() up-complete /\-complete distributive Heyting complemented Boolean with_suprema with_infima complete satisfying_MC meet-continuous RelStr

the carrier of (BoolePoset {L}) is non empty set

[: the carrier of L, the carrier of (BoolePoset {L}):] is non empty Relation-like set

bool [: the carrier of L, the carrier of (BoolePoset {L}):] is non empty set

l1 is Relation-like the carrier of L -defined the carrier of (BoolePoset {L}) -valued Function-like V32( the carrier of L, the carrier of (BoolePoset {L})) Element of bool [: the carrier of L, the carrier of (BoolePoset {L}):]

bool {L} is non empty finite V41() set

InclPoset (bool {L}) is non empty strict V110() reflexive transitive antisymmetric RelStr

the carrier of (InclPoset (bool {L})) is non empty set

{{},{L}} is non empty finite V41() set

dom l1 is Element of bool the carrier of L

bool the carrier of L is non empty set

Y is Element of the carrier of L

Y is Element of the carrier of L

{Y,Y} is non empty finite Element of bool the carrier of L

l1 .: {Y,Y} is non empty finite Element of bool the carrier of (BoolePoset {L})

bool the carrier of (BoolePoset {L}) is non empty set

l1 . Y is Element of the carrier of (BoolePoset {L})

l1 . Y is Element of the carrier of (BoolePoset {L})

{(l1 . Y),(l1 . Y)} is non empty finite Element of bool the carrier of (BoolePoset {L})

Y "/\" Y is Element of the carrier of L

(l1 . Y) "/\" (l1 . Y) is Element of the carrier of (BoolePoset {L})

{} /\ {} is Relation-like finite set

l1 . (Y "/\" Y) is Element of the carrier of (BoolePoset {L})

Y "/\" Y is Element of the carrier of L

l1 . (Y "/\" Y) is Element of the carrier of (BoolePoset {L})

(l1 . Y) "/\" (l1 . Y) is Element of the carrier of (BoolePoset {L})

{L} /\ {L} is finite set

Y "/\" Y is Element of the carrier of L

(l1 . Y) "/\" (l1 . Y) is Element of the carrier of (BoolePoset {L})

{} /\ {L} is Relation-like finite set

l1 . (Y "/\" Y) is Element of the carrier of (BoolePoset {L})

Y "/\" Y is Element of the carrier of L

(l1 . Y) "/\" (l1 . Y) is Element of the carrier of (BoolePoset {L})

{L} /\ {} is Relation-like finite set

l1 . (Y "/\" Y) is Element of the carrier of (BoolePoset {L})

(l1 . Y) "/\" (l1 . Y) is Element of the carrier of (BoolePoset {L})

Y "/\" Y is Element of the carrier of L

l1 . (Y "/\" Y) is Element of the carrier of (BoolePoset {L})

(l1 . Y) "/\" (l1 . Y) is Element of the carrier of (BoolePoset {L})

Y "/\" Y is Element of the carrier of L

l1 . (Y "/\" Y) is Element of the carrier of (BoolePoset {L})

"/\" ((l1 .: {Y,Y}),(BoolePoset {L})) is Element of the carrier of (BoolePoset {L})

"/\" ({Y,Y},L) is Element of the carrier of L

l1 . ("/\" ({Y,Y},L)) is Element of the carrier of (BoolePoset {L})

Y is Element of the carrier of L

Y is Element of the carrier of L

{Y,Y} is non empty finite Element of bool the carrier of L

l1 .: {Y,Y} is non empty finite Element of bool the carrier of (BoolePoset {L})

bool the carrier of (BoolePoset {L}) is non empty set

l1 . Y is Element of the carrier of (BoolePoset {L})

l1 . Y is Element of the carrier of (BoolePoset {L})

{(l1 . Y),(l1 . Y)} is non empty finite Element of bool the carrier of (BoolePoset {L})

Y "\/" Y is Element of the carrier of L

(l1 . Y) "\/" (l1 . Y) is Element of the carrier of (BoolePoset {L})

{} \/ {} is Relation-like finite V41() set

l1 . (Y "\/" Y) is Element of the carrier of (BoolePoset {L})

Y "\/" Y is Element of the carrier of L

l1 . (Y "\/" Y) is Element of the carrier of (BoolePoset {L})

(l1 . Y) "\/" (l1 . Y) is Element of the carrier of (BoolePoset {L})

{L} \/ {L} is non empty finite set

Y "\/" Y is Element of the carrier of L

l1 . (Y "\/" Y) is Element of the carrier of (BoolePoset {L})

(l1 . Y) "\/" (l1 . Y) is Element of the carrier of (BoolePoset {L})

{} \/ {L} is non empty finite set

Y "\/" Y is Element of the carrier of L

l1 . (Y "\/" Y) is Element of the carrier of (BoolePoset {L})

(l1 . Y) "\/" (l1 . Y) is Element of the carrier of (BoolePoset {L})

{L} \/ {} is non empty finite set

(l1 . Y) "\/" (l1 . Y) is Element of the carrier of (BoolePoset {L})

Y "\/" Y is Element of the carrier of L

l1 . (Y "\/" Y) is Element of the carrier of (BoolePoset {L})

(l1 . Y) "\/" (l1 . Y) is Element of the carrier of (BoolePoset {L})

Y "\/" Y is Element of the carrier of L

l1 . (Y "\/" Y) is Element of the carrier of (BoolePoset {L})

"\/" ((l1 .: {Y,Y}),(BoolePoset {L})) is Element of the carrier of (BoolePoset {L})

"\/" ({Y,Y},L) is Element of the carrier of L

l1 . ("\/" ({Y,Y},L)) is Element of the carrier of (BoolePoset {L})

L is Element of the carrier of L

l1 is Element of the carrier of L

L "/\" l1 is Element of the carrier of L

BoolePoset {{}} is non empty strict V110() reflexive transitive antisymmetric lower-bounded upper-bounded V167() up-complete /\-complete distributive Heyting complemented Boolean with_suprema with_infima complete satisfying_MC meet-continuous RelStr

the carrier of (BoolePoset {{}}) is non empty set

bool {{}} is non empty finite V41() set

InclPoset (bool {{}}) is non empty strict V110() reflexive transitive antisymmetric RelStr

the carrier of (InclPoset (bool {{}})) is non empty set

{{},{{}}} is non empty finite V41() set

Y is Element of the carrier of L

x is Element of the carrier of (BoolePoset {{}})

x is Element of the carrier of (BoolePoset {{}})

Y is Element of the carrier of (BoolePoset {{}})

[: the carrier of L, the carrier of (BoolePoset {{}}):] is non empty Relation-like set

bool [: the carrier of L, the carrier of (BoolePoset {{}}):] is non empty set

Y is Relation-like the carrier of L -defined the carrier of (BoolePoset {{}}) -valued Function-like V32( the carrier of L, the carrier of (BoolePoset {{}})) Element of bool [: the carrier of L, the carrier of (BoolePoset {{}}):]

{L,l1} is non empty finite Element of bool the carrier of L

bool the carrier of L is non empty set

dom Y is Element of bool the carrier of L

Y .: {L,l1} is non empty finite Element of bool the carrier of (BoolePoset {{}})

bool the carrier of (BoolePoset {{}}) is non empty set

Y . L is Element of the carrier of (BoolePoset {{}})

Y . l1 is Element of the carrier of (BoolePoset {{}})

{(Y . L),(Y . l1)} is non empty finite Element of bool the carrier of (BoolePoset {{}})

L "/\" l1 is Element of the carrier of L

Y . (L "/\" l1) is Element of the carrier of (BoolePoset {{}})

"/\" ({L,l1},L) is Element of the carrier of L

Y . ("/\" ({L,l1},L)) is Element of the carrier of (BoolePoset {{}})

"/\" ({(Y . L),(Y . l1)},(BoolePoset {{}})) is Element of the carrier of (BoolePoset {{}})

(Y . L) "/\" (Y . l1) is Element of the carrier of (BoolePoset {{}})

(Y . L) /\ (Y . l1) is set

L is non empty V110() reflexive transitive antisymmetric upper-bounded with_suprema with_infima RelStr

the carrier of L is non empty set

Top L is Element of the carrier of L

bool the carrier of L is non empty set

L is Element of the carrier of L

downarrow L is non empty directed lower Element of bool the carrier of L

{L} is non empty trivial finite V44(1) Element of bool the carrier of L

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

(downarrow L) ` is Element of bool the carrier of L

the carrier of L \ (downarrow L) is set

the carrier of L \ (downarrow L) is Element of bool the carrier of L

Y is Element of the carrier of L

l1 is Element of bool the carrier of L

Y is Element of the carrier of L

Y "/\" Y is Element of the carrier of L

Y is Element of the carrier of L

Y is Element of the carrier of L

Y is Element of the carrier of L

Y is Element of the carrier of L

Y "/\" Y is Element of the carrier of L

Y "/\" Y is Element of the carrier of L

l1 is Element of bool the carrier of L

x is Element of the carrier of L

L is non empty V110() reflexive transitive antisymmetric distributive with_suprema with_infima RelStr

the carrier of L is non empty set

L is Element of the carrier of L

L is Element of the carrier of L

l1 is Element of the carrier of L

L "/\" l1 is Element of the carrier of L

L "/\" l1 is Element of the carrier of L

L "\/" (L "/\" l1) is Element of the carrier of L

L "\/" L is Element of the carrier of L

L "\/" l1 is Element of the carrier of L

(L "\/" L) "/\" (L "\/" l1) is Element of the carrier of L

L is non empty V110() reflexive transitive antisymmetric distributive with_suprema with_infima RelStr

(L) is Element of bool the carrier of L

the carrier of L is non empty set

bool the carrier of L is non empty set

(L) is Element of bool the carrier of L

L is set

L is Element of (L)

l1 is Element of the carrier of L

L is set

L is Element of (L)

l1 is Element of the carrier of L

L is non empty V110() reflexive transitive antisymmetric lower-bounded upper-bounded V167() distributive Heyting complemented Boolean with_suprema with_infima RelStr

the carrier of L is non empty set

Top L is Element of the carrier of L

L is Element of the carrier of L

L is Element of the carrier of L

l1 is Element of the carrier of L

L "/\" l1 is Element of the carrier of L

Bottom L is Element of the carrier of L

L "\/" l1 is Element of the carrier of L

L is Element of the carrier of L

l1 is Element of the carrier of L

L "/\" l1 is Element of the carrier of L

L "/\" l1 is Element of the carrier of L

L "\/" (L "/\" l1) is Element of the carrier of L

L "\/" L is Element of the carrier of L

L "\/" l1 is Element of the carrier of L

(L "\/" L) "/\" (L "\/" l1) is Element of the carrier of L

L is non empty V110() reflexive transitive antisymmetric lower-bounded upper-bounded V167() up-complete /\-complete distributive with_suprema with_infima complete satisfying_axiom_of_approximation continuous RelStr

the carrier of L is non empty set

Top L is Element of the carrier of L

bool the carrier of L is non empty set

L is Element of the carrier of L

downarrow L is non empty directed lower Element of bool the carrier of L

{L} is non empty trivial finite V44(1) Element of bool the carrier of L

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

(downarrow L) ` is Element of bool the carrier of L

the carrier of L \ (downarrow L) is set

l1 is Element of the carrier of L

waybelow l1 is non empty directed lower Element of bool the carrier of L

Y is Element of the carrier of L

waybelow Y is non empty directed lower Element of bool the carrier of L

l1 is Element of the carrier of L

Y is Element of the carrier of L

l1 is non empty filtered upper (L) Element of bool the carrier of L

l1 ` is Element of bool the carrier of L

the carrier of L \ l1 is set

Y is Element of the carrier of L

l1 is non empty filtered upper (L) Element of bool the carrier of L

l1 ` is Element of bool the carrier of L

the carrier of L \ l1 is set

l1 is Element of the carrier of L

Y is Element of the carrier of L

l1 "/\" Y is Element of the carrier of L

L "\/" (l1 "/\" Y) is Element of the carrier of L

L "\/" l1 is Element of the carrier of L

L "\/" Y is Element of the carrier of L

(L "\/" l1) "/\" (L "\/" Y) is Element of the carrier of L

BoolePoset {{}} is non empty strict V110() reflexive transitive antisymmetric lower-bounded upper-bounded V167() up-complete /\-complete distributive Heyting complemented Boolean with_suprema with_infima complete satisfying_MC meet-continuous RelStr

the carrier of (BoolePoset {{}}) is non empty set

L is RelStr

the carrier of L is set

bool the carrier of L is non empty set

[: the carrier of L, the carrier of (BoolePoset {{}}):] is Relation-like set

bool [: the carrier of L, the carrier of (BoolePoset {{}}):] is non empty set

L is Element of bool the carrier of L

chi (L, the carrier of L) is Relation-like the carrier of L -defined {{},1} -valued Function-like V32( the carrier of L,{{},1}) Element of bool [: the carrier of L,{{},1}:]

[: the carrier of L,{{},1}:] is Relation-like set

bool [: the carrier of L,{{},1}:] is non empty set

bool {{}} is non empty finite V41() set

InclPoset (bool {{}}) is non empty strict V110() reflexive transitive antisymmetric RelStr

the carrier of (InclPoset (bool {{}})) is non empty set

{0,1} is non empty finite V41() Element of bool NAT

L is non empty RelStr

the carrier of L is non empty set

L is Element of the carrier of L

downarrow L is Element of bool the carrier of L

bool the carrier of L is non empty set

{L} is non empty trivial finite V44(1) Element of bool the carrier of L

downarrow {L} is Element of bool the carrier of L

(downarrow L) ` is Element of bool the carrier of L

the carrier of L \ (downarrow L) is set

chi (((downarrow L) `), the carrier of L) is Relation-like the carrier of L -defined {{},1} -valued Function-like V32( the carrier of L,{{},1}) Element of bool [: the carrier of L,{{},1}:]

[: the carrier of L,{{},1}:] is non empty Relation-like set

bool [: the carrier of L,{{},1}:] is non empty set

L is Element of the carrier of L

(chi (((downarrow L) `), the carrier of L)) . L is finite Element of {{},1}

L is non empty V110() reflexive transitive antisymmetric upper-bounded with_suprema with_infima RelStr

the carrier of L is non empty set

[: the carrier of L, the carrier of (BoolePoset {{}}):] is non empty Relation-like set

bool [: the carrier of L, the carrier of (BoolePoset {{}}):] is non empty set

L is Relation-like the carrier of L -defined the carrier of (BoolePoset {{}}) -valued Function-like V32( the carrier of L, the carrier of (BoolePoset {{}})) Element of bool [: the carrier of L, the carrier of (BoolePoset {{}}):]

L is (L) Element of the carrier of L

downarrow L is non empty directed lower Element of bool the carrier of L

bool the carrier of L is non empty set

{L} is non empty trivial finite V44(1) Element of bool the carrier of L

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

(downarrow L) ` is Element of bool the carrier of L

the carrier of L \ (downarrow L) is set

chi (((downarrow L) `), the carrier of L) is Relation-like the carrier of L -defined {{},1} -valued Function-like V32( the carrier of L,{{},1}) Element of bool [: the carrier of L,{{},1}:]

[: the carrier of L,{{},1}:] is non empty Relation-like set

bool [: the carrier of L,{{},1}:] is non empty set

l1 is Element of the carrier of L

L . l1 is Element of the carrier of (BoolePoset {{}})

Y is Element of the carrier of L

L . Y is Element of the carrier of (BoolePoset {{}})

L is non empty V110() reflexive transitive antisymmetric lower-bounded upper-bounded V167() up-complete /\-complete with_suprema with_infima complete RelStr

(L) is Element of bool the carrier of L

the carrier of L is non empty set

bool the carrier of L is non empty set

{ (chi (((downarrow b

the (L) Element of the carrier of L is (L) Element of the carrier of L

downarrow the (L) Element of the carrier of L is non empty directed lower Element of bool the carrier of L

{ the (L) Element of the carrier of L} is non