:: WAYBEL35 semantic presentation

REAL is set

NAT is non empty V16() V17() V18() V37() cardinal limit_cardinal Element of bool REAL

bool REAL is non empty set

NAT is non empty V16() V17() V18() V37() cardinal limit_cardinal set

bool NAT is non empty V37() set

{} is set

the empty trivial V16() V17() V18() V20() V21() V22() V37() cardinal {} -element set is empty trivial V16() V17() V18() V20() V21() V22() V37() cardinal {} -element set

1 is non empty V16() V17() V18() V22() V37() cardinal Element of NAT

{{},1} is set

bool NAT is non empty V37() set

R is set

L is set

{L} is non empty trivial 1 -element set

C is set

{L} \/ C is set

L is RelStr

the carrier of L is set

[: the carrier of L, the carrier of L:] is set

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

IntRel L is Relation-like the carrier of L -defined the carrier of L -valued auxiliary(i) Element of bool [: the carrier of L, the carrier of L:]

L is transitive RelStr

the carrier of L is set

[: the carrier of L, the carrier of L:] is set

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

IntRel L is Relation-like the carrier of L -defined the carrier of L -valued auxiliary(i) auxiliary(ii) Element of bool [: the carrier of L, the carrier of L:]

L is non empty antisymmetric with_suprema RelStr

the carrier of L is non empty set

[: the carrier of L, the carrier of L:] is non empty set

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

IntRel L is Relation-like the carrier of L -defined the carrier of L -valued auxiliary(i) auxiliary(iii) Element of bool [: the carrier of L, the carrier of L:]

L is non empty antisymmetric lower-bounded RelStr

the carrier of L is non empty set

[: the carrier of L, the carrier of L:] is non empty set

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

IntRel L is Relation-like the carrier of L -defined the carrier of L -valued auxiliary(i) auxiliary(iv) Element of bool [: the carrier of L, the carrier of L:]

L is non empty RelStr

the carrier of L is non empty set

[: the carrier of L, the carrier of L:] is non empty set

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

L is non empty RelStr

the carrier of L is non empty set

[: the carrier of L, the carrier of L:] is non empty set

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

R is Relation-like the carrier of L -defined the carrier of L -valued Element of bool [: the carrier of L, the carrier of L:]

R is Relation-like the carrier of L -defined the carrier of L -valued Element of bool [: the carrier of L, the carrier of L:]

L is non empty RelStr

the carrier of L is non empty set

[: the carrier of L, the carrier of L:] is non empty set

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

R is Relation-like the carrier of L -defined the carrier of L -valued Element of bool [: the carrier of L, the carrier of L:]

R is Relation-like the carrier of L -defined the carrier of L -valued Element of bool [: the carrier of L, the carrier of L:]

L is non empty transitive antisymmetric lower-bounded RelStr

the carrier of L is non empty set

[: the carrier of L, the carrier of L:] is non empty set

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

IntRel L is Relation-like the carrier of L -defined the carrier of L -valued auxiliary(i) auxiliary(ii) auxiliary(iv) (L) Element of bool [: the carrier of L, the carrier of L:]

L is non empty reflexive transitive antisymmetric lower-bounded with_suprema RelStr

the carrier of L is non empty set

[: the carrier of L, the carrier of L:] is non empty set

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

LOWER L is non empty set

InclPoset (LOWER L) is non empty strict reflexive transitive antisymmetric RelStr

the carrier of (InclPoset (LOWER L)) is non empty set

[: the carrier of L, the carrier of (InclPoset (LOWER L)):] is non empty set

bool [: the carrier of L, the carrier of (InclPoset (LOWER L)):] is non empty set

R is Relation-like the carrier of L -defined the carrier of L -valued auxiliary(ii) Element of bool [: the carrier of L, the carrier of L:]

bool the carrier of L is non empty set

C is Element of the carrier of L

R -below C is lower Element of bool the carrier of L

{ b

a is lower Element of bool the carrier of L

C is Relation-like the carrier of L -defined the carrier of (InclPoset (LOWER L)) -valued Function-like V31( the carrier of L, the carrier of (InclPoset (LOWER L))) Element of bool [: the carrier of L, the carrier of (InclPoset (LOWER L)):]

a is Element of the carrier of L

C . a is Element of the carrier of (InclPoset (LOWER L))

R -below a is lower Element of bool the carrier of L

C is Relation-like the carrier of L -defined the carrier of (InclPoset (LOWER L)) -valued Function-like V31( the carrier of L, the carrier of (InclPoset (LOWER L))) Element of bool [: the carrier of L, the carrier of (InclPoset (LOWER L)):]

a is Relation-like the carrier of L -defined the carrier of (InclPoset (LOWER L)) -valued Function-like V31( the carrier of L, the carrier of (InclPoset (LOWER L))) Element of bool [: the carrier of L, the carrier of (InclPoset (LOWER L)):]

b is set

C . b is set

a . b is set

d is Element of the carrier of L

R -below d is lower Element of bool the carrier of L

bool the carrier of L is non empty set

L is non empty reflexive transitive antisymmetric lower-bounded with_suprema RelStr

the carrier of L is non empty set

[: the carrier of L, the carrier of L:] is non empty set

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

LOWER L is non empty set

InclPoset (LOWER L) is non empty strict reflexive transitive antisymmetric RelStr

R is Relation-like the carrier of L -defined the carrier of L -valued auxiliary(ii) Element of bool [: the carrier of L, the carrier of L:]

(L,R) is Relation-like the carrier of L -defined the carrier of (InclPoset (LOWER L)) -valued Function-like V31( the carrier of L, the carrier of (InclPoset (LOWER L))) Element of bool [: the carrier of L, the carrier of (InclPoset (LOWER L)):]

the carrier of (InclPoset (LOWER L)) is non empty set

[: the carrier of L, the carrier of (InclPoset (LOWER L)):] is non empty set

bool [: the carrier of L, the carrier of (InclPoset (LOWER L)):] is non empty set

C is Element of the carrier of L

a is Element of the carrier of L

(L,R) . C is Element of the carrier of (InclPoset (LOWER L))

(L,R) . a is Element of the carrier of (InclPoset (LOWER L))

R -below a is lower Element of bool the carrier of L

bool the carrier of L is non empty set

R -below C is lower Element of bool the carrier of L

L is 1-sorted

the carrier of L is set

[: the carrier of L, the carrier of L:] is set

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

bool the carrier of L is non empty set

R is Relation-like the carrier of L -defined the carrier of L -valued Element of bool [: the carrier of L, the carrier of L:]

{} L is empty trivial V16() V17() V18() V20() V21() V22() V37() cardinal {} -element Element of bool the carrier of L

C is set

a is set

[C,a] is non empty set

{C,a} is set

{C} is non empty trivial 1 -element set

{{C,a},{C}} is set

[a,C] is non empty set

{a,C} is set

{a} is non empty trivial 1 -element set

{{a,C},{a}} is set

L is 1-sorted

the carrier of L is set

bool the carrier of L is non empty set

[: the carrier of L, the carrier of L:] is set

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

R is trivial Element of bool the carrier of L

C is Relation-like the carrier of L -defined the carrier of L -valued Element of bool [: the carrier of L, the carrier of L:]

a is set

b is set

[a,b] is non empty set

{a,b} is set

{a} is non empty trivial 1 -element set

{{a,b},{a}} is set

[b,a] is non empty set

{b,a} is set

{b} is non empty trivial 1 -element set

{{b,a},{b}} is set

L is non empty 1-sorted

the carrier of L is non empty set

[: the carrier of L, the carrier of L:] is non empty set

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

R is Relation-like the carrier of L -defined the carrier of L -valued Element of bool [: the carrier of L, the carrier of L:]

bool the carrier of L is non empty set

the non empty trivial 1 -element Element of bool the carrier of L is non empty trivial 1 -element Element of bool the carrier of L

a is (L,R)

L is antisymmetric RelStr

the carrier of L is set

[: the carrier of L, the carrier of L:] is set

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

R is Relation-like the carrier of L -defined the carrier of L -valued auxiliary(i) Element of bool [: the carrier of L, the carrier of L:]

C is (L,R)

a is Element of the carrier of L

b is Element of the carrier of L

[a,b] is non empty set

{a,b} is set

{a} is non empty trivial 1 -element set

{{a,b},{a}} is set

[b,a] is non empty set

{b,a} is set

{b} is non empty trivial 1 -element set

{{b,a},{b}} is set

L is antisymmetric RelStr

the carrier of L is set

[: the carrier of L, the carrier of L:] is set

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

R is Relation-like the carrier of L -defined the carrier of L -valued auxiliary(i) Element of bool [: the carrier of L, the carrier of L:]

C is Element of the carrier of L

a is Element of the carrier of L

[C,a] is non empty set

{C,a} is set

{C} is non empty trivial 1 -element set

{{C,a},{C}} is set

[a,C] is non empty set

{a,C} is set

{a} is non empty trivial 1 -element set

{{a,C},{a}} is set

L is non empty antisymmetric lower-bounded RelStr

the carrier of L is non empty set

[: the carrier of L, the carrier of L:] is non empty set

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

Bottom L is Element of the carrier of L

R is Element of the carrier of L

{(Bottom L),R} is Element of bool the carrier of L

bool the carrier of L is non empty set

C is Relation-like the carrier of L -defined the carrier of L -valued auxiliary(iv) Element of bool [: the carrier of L, the carrier of L:]

a is set

b is set

[a,b] is non empty set

{a,b} is set

{a} is non empty trivial 1 -element set

{{a,b},{a}} is set

[b,a] is non empty set

{b,a} is set

{b} is non empty trivial 1 -element set

{{b,a},{b}} is set

L is non empty antisymmetric lower-bounded RelStr

the carrier of L is non empty set

[: the carrier of L, the carrier of L:] is non empty set

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

Bottom L is Element of the carrier of L

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

bool the carrier of L is non empty set

R is Relation-like the carrier of L -defined the carrier of L -valued auxiliary(iv) Element of bool [: the carrier of L, the carrier of L:]

C is (L,R)

C \/ {(Bottom L)} is Element of bool the carrier of L

b is set

d is set

[b,d] is non empty set

{b,d} is set

{b} is non empty trivial 1 -element set

{{b,d},{b}} is set

[d,b] is non empty set

{d,b} is set

{d} is non empty trivial 1 -element set

{{d,b},{d}} is set

c

y is Element of the carrier of L

c

y is Element of the carrier of L

c

y is Element of the carrier of L

c

y is Element of the carrier of L

c

y is Element of the carrier of L

L is 1-sorted

the carrier of L is set

[: the carrier of L, the carrier of L:] is set

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

R is Relation-like the carrier of L -defined the carrier of L -valued Element of bool [: the carrier of L, the carrier of L:]

L is 1-sorted

the carrier of L is set

[: the carrier of L, the carrier of L:] is set

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

R is Relation-like the carrier of L -defined the carrier of L -valued Element of bool [: the carrier of L, the carrier of L:]

C is set

bool the carrier of L is non empty set

a is set

b is set

d is set

L is 1-sorted

the carrier of L is set

[: the carrier of L, the carrier of L:] is set

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

R is Relation-like the carrier of L -defined the carrier of L -valued Element of bool [: the carrier of L, the carrier of L:]

C is (L,R)

(L,R,C) is set

L is 1-sorted

the carrier of L is set

[: the carrier of L, the carrier of L:] is set

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

R is Relation-like the carrier of L -defined the carrier of L -valued Element of bool [: the carrier of L, the carrier of L:]

C is (L,R)

(L,R,C) is non empty set

RelIncl (L,R,C) is Relation-like (L,R,C) -defined (L,R,C) -valued V27((L,R,C)) reflexive antisymmetric transitive Element of bool [:(L,R,C),(L,R,C):]

[:(L,R,C),(L,R,C):] is non empty set

bool [:(L,R,C),(L,R,C):] is non empty set

field (RelIncl (L,R,C)) is set

b is set

(RelIncl (L,R,C)) |_2 b is Relation-like set

d is set

[d,C] is non empty set

{d,C} is set

{d} is non empty trivial 1 -element set

{{d,C},{d}} is set

union b is set

d is set

c

y is set

bool the carrier of L is non empty set

c

field ((RelIncl (L,R,C)) |_2 b) is set

RelIncl b is Relation-like b -defined b -valued V27(b) reflexive antisymmetric transitive Element of bool [:b,b:]

[:b,b:] is set

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

y is set

c

[y,c

{y,c

{y} is non empty trivial 1 -element set

{{y,c

[c

{c

{c

{{c

field (RelIncl b) is set

f is set

f is set

[f,f] is non empty set

{f,f} is set

{f} is non empty trivial 1 -element set

{{f,f},{f}} is set

[f,f] is non empty set

{f,f} is set

{f} is non empty trivial 1 -element set

{{f,f},{f}} is set

y is set

c

y is set

[y,d] is non empty set

{y,d} is set

{y} is non empty trivial 1 -element set

{{y,d},{y}} is set

b is set

L is non empty transitive RelStr

the carrier of L is non empty set

bool the carrier of L is non empty set

R is non empty Element of bool the carrier of L

bool R is non empty set

subrelstr R is non empty strict transitive V134(L) SubRelStr of L

C is Element of bool R

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

"\/" (C,(subrelstr R)) is Element of the carrier of (subrelstr R)

the carrier of (subrelstr R) is non empty set

L is non empty reflexive transitive antisymmetric RelStr

the carrier of L is non empty set

[: the carrier of L, the carrier of L:] is non empty set

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

R is Relation-like the carrier of L -defined the carrier of L -valued auxiliary(i) auxiliary(ii) Element of bool [: the carrier of L, the carrier of L:]

C is non empty (L,R)

bool C is non empty set

subrelstr C is non empty strict reflexive transitive antisymmetric V134(L) SubRelStr of L

the carrier of (subrelstr C) is non empty set

a is Element of bool C

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

{("\/" (a,L))} is non empty trivial 1 -element Element of bool the carrier of L

bool the carrier of L is non empty set

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

d is Element of the carrier of L

[d,("\/" (a,L))] is non empty Element of [: the carrier of L, the carrier of L:]

{d,("\/" (a,L))} is set

{d} is non empty trivial 1 -element set

{{d,("\/" (a,L))},{d}} is set

[("\/" (a,L)),d] is non empty Element of [: the carrier of L, the carrier of L:]

{("\/" (a,L)),d} is set

{("\/" (a,L))} is non empty trivial 1 -element set

{{("\/" (a,L)),d},{("\/" (a,L))}} is set

c

[d,c

{d,c

{{d,c

[c

{c

{c

{{c

[d,c

{d,c

{{d,c

[c

{c

{c

{{c

d is set

c

[d,c

{d,c

{d} is non empty trivial 1 -element set

{{d,c

[c

{c

{c

{{c

y is Element of the carrier of L

c

y is Element of the carrier of L

c

y is Element of the carrier of L

c

y is Element of the carrier of L

c

y is Element of the carrier of L

c

d is Element of the carrier of L

[("\/" (a,L)),d] is non empty Element of [: the carrier of L, the carrier of L:]

{("\/" (a,L)),d} is set

{("\/" (a,L))} is non empty trivial 1 -element set

{{("\/" (a,L)),d},{("\/" (a,L))}} is set

d is Element of the carrier of L

[("\/" (a,L)),d] is non empty Element of [: the carrier of L, the carrier of L:]

{("\/" (a,L)),d} is set

{("\/" (a,L))} is non empty trivial 1 -element set

{{("\/" (a,L)),d},{("\/" (a,L))}} is set

c

y is Element of the carrier of (subrelstr C)

c

y is Element of the carrier of (subrelstr C)

c

[c

[: the carrier of (subrelstr C), the carrier of (subrelstr C):] is non empty set

{c

{c

{{c

[y,c

{y,c

{y} is non empty trivial 1 -element set

{{y,c

L is non empty reflexive transitive antisymmetric RelStr

the carrier of L is non empty set

[: the carrier of L, the carrier of L:] is non empty set

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

R is Relation-like the carrier of L -defined the carrier of L -valued auxiliary(i) auxiliary(ii) Element of bool [: the carrier of L, the carrier of L:]

C is non empty (L,R)

bool C is non empty set

subrelstr C is non empty strict reflexive transitive antisymmetric V134(L) SubRelStr of L

a is Element of bool C

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

the carrier of (subrelstr C) is non empty set

d is Element of the carrier of L

[("\/" (a,L)),d] is non empty Element of [: the carrier of L, the carrier of L:]

{("\/" (a,L)),d} is set

{("\/" (a,L))} is non empty trivial 1 -element set

{{("\/" (a,L)),d},{("\/" (a,L))}} is set

c

L is non empty reflexive transitive antisymmetric RelStr

the carrier of L is non empty set

[: the carrier of L, the carrier of L:] is non empty set

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

R is Relation-like the carrier of L -defined the carrier of L -valued auxiliary(i) auxiliary(ii) Element of bool [: the carrier of L, the carrier of L:]

C is non empty (L,R)

bool C is non empty set

subrelstr C is non empty strict reflexive transitive antisymmetric V134(L) SubRelStr of L

a is Element of bool C

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

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

bool the carrier of L is non empty set

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

"\/" (a,(subrelstr C)) is Element of the carrier of (subrelstr C)

the carrier of (subrelstr C) is non empty set

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

y is Element of the carrier of L

c

c

c

[("\/" (a,L)),c

{("\/" (a,L)),c

{("\/" (a,L))} is non empty trivial 1 -element set

{{("\/" (a,L)),c

f is Element of the carrier of L

f is Element of the carrier of L

[f,c

{f,c

{f} is non empty trivial 1 -element set

{{f,c

[c

{c

{c

{{c

f is Element of the carrier of (subrelstr C)

L is non empty reflexive transitive antisymmetric lower-bounded upper-bounded V133() 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 set

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

R is Relation-like the carrier of L -defined the carrier of L -valued transitive auxiliary(i) auxiliary(ii) Element of bool [: the carrier of L, the carrier of L:]

C is non empty (L,R)

subrelstr C is non empty strict reflexive transitive antisymmetric V134(L) SubRelStr of L

the carrier of (subrelstr C) is non empty set

bool the carrier of (subrelstr C) is non empty set

a is Element of bool the carrier of (subrelstr C)

bool C is non empty set

L is non empty antisymmetric lower-bounded RelStr

the carrier of L is non empty set

[: the carrier of L, the carrier of L:] is non empty set

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

Bottom L is Element of the carrier of L

R is Relation-like the carrier of L -defined the carrier of L -valued auxiliary(iv) Element of bool [: the carrier of L, the carrier of L:]

C is (L,R)

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

bool the carrier of L is non empty set

C \/ {(Bottom L)} is Element of bool the carrier of L

L is non empty reflexive transitive antisymmetric upper-bounded RelStr

the carrier of L is non empty set

[: the carrier of L, the carrier of L:] is non empty set

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

Top L is Element of the carrier of L

[(Top L),(Top L)] is non empty Element of [: the carrier of L, the carrier of L:]

{(Top L),(Top L)} is set

{(Top L)} is non empty trivial 1 -element set

{{(Top L),(Top L)},{(Top L)}} is set

R is Relation-like the carrier of L -defined the carrier of L -valued auxiliary(ii) Element of bool [: the carrier of L, the carrier of L:]

C is (L,R)

a is Element of the carrier of L

[a,(Top L)] is non empty Element of [: the carrier of L, the carrier of L:]

{a,(Top L)} is set

{a} is non empty trivial 1 -element set

{{a,(Top L)},{a}} is set

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

bool the carrier of L is non empty set

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

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

b is set

d is set

[b,d] is non empty set

{b,d} is set

{b} is non empty trivial 1 -element set

{{b,d},{b}} is set

[d,b] is non empty set

{d,b} is set

{d} is non empty trivial 1 -element set

{{d,b},{d}} is set

c

c

L is RelStr

the carrier of L is set

[: the carrier of L, the carrier of L:] is set

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

L is RelStr

the carrier of L is set

[: the carrier of L, the carrier of L:] is set

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

R is Relation-like the carrier of L -defined the carrier of L -valued Element of bool [: the carrier of L, the carrier of L:]

L is RelStr

the carrier of L is set

[: the carrier of L, the carrier of L:] is set

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

R is set

C is Relation-like the carrier of L -defined the carrier of L -valued auxiliary(i) Element of bool [: the carrier of L, the carrier of L:]

a is Element of the carrier of L

b is Element of the carrier of L

[a,b] is non empty set

{a,b} is set

{a} is non empty trivial 1 -element set

{{a,b},{a}} is set

d is Element of the carrier of L

[a,d] is non empty set

{a,d} is set

{{a,d},{a}} is set

[d,b] is non empty set

{d,b} is set

{d} is non empty trivial 1 -element set

{{d,b},{d}} is set

L is RelStr

the carrier of L is set

[: the carrier of L, the carrier of L:] is set

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

R is Relation-like the carrier of L -defined the carrier of L -valued Element of bool [: the carrier of L, the carrier of L:]

C is (L,R)

a is Element of the carrier of L

b is Element of the carrier of L

[a,b] is non empty set

{a,b} is set

{a} is non empty trivial 1 -element set

{{a,b},{a}} is set

L is non empty RelStr

the carrier of L is non empty set

[: the carrier of L, the carrier of L:] is non empty set

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

R is Relation-like the carrier of L -defined the carrier of L -valued Element of bool [: the carrier of L, the carrier of L:]

bool the carrier of L is non empty set

the non empty trivial 1 -element Element of bool the carrier of L is non empty trivial 1 -element Element of bool the carrier of L

a is (L,R)

L is non empty reflexive transitive antisymmetric lower-bounded with_suprema RelStr

the carrier of L is non empty set

[: the carrier of L, the carrier of L:] is non empty set

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

R is Relation-like the carrier of L -defined the carrier of L -valued transitive auxiliary(i) auxiliary(ii) Element of bool [: the carrier of L, the carrier of L:]

C is (L,R)

a is Element of the carrier of L

b is Element of the carrier of L

[a,b] is non empty set

{a,b} is set

{a} is non empty trivial 1 -element set

{{a,b},{a}} is set

[a,b] is non empty Element of [: the carrier of L, the carrier of L:]

d is Element of the carrier of L

[a,d] is non empty Element of [: the carrier of L, the carrier of L:]

{a,d} is set

{{a,d},{a}} is set

[d,b] is non empty Element of [: the carrier of L, the carrier of L:]

{d,b} is set

{d} is non empty trivial 1 -element set

{{d,b},{d}} is set

{d} is non empty trivial 1 -element Element of bool the carrier of L

bool the carrier of L is non empty set

C \/ {d} is Element of bool the carrier of L

c

y is set

[c

{c

{c

{{c

[y,c

{y,c

{y} is non empty trivial 1 -element set

{{y,c

c

[a,c

{a,c

{{a,c

[c

{c

{c

{{c

[c

{c

{c

{{c

[b,c

{b,c

{b} is non empty trivial 1 -element set

{{b,c

[a,c

{a,c

{{a,c

[c

{c

{c

{{c

c

[a,c

{a,c

{{a,c

[c

{c

{c

{{c

[c

{c

{c

{{c

[b,c

{b,c

{b} is non empty trivial 1 -element set

{{b,c

[a,c

{a,c

{{a,c

[c

{c

{c

{{c

L is Relation-like set

C is set

{C} is non empty trivial 1 -element set

L " {C} is set

R is set

(L " {C}) /\ R is set

L is Relation-like set

C is set

R is set

a is set

(L,R,a) is set

{a} is non empty trivial 1 -element set

L " {a} is set

(L " {a}) /\ R is set

[C,a] is non empty set

{C,a} is set

{C} is non empty trivial 1 -element set

{{C,a},{C}} is set

b is set

[C,b] is non empty set

{C,b} is set

{{C,b},{C}} is set

L is 1-sorted

the carrier of L is set

[: the carrier of L, the carrier of L:] is set

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

R is Relation-like the carrier of L -defined the carrier of L -valued Element of bool [: the carrier of L, the carrier of L:]

C is set

a is set

(R,C,a) is set

{a} is non empty trivial 1 -element set

R " {a} is set

(R " {a}) /\ C is set

bool the carrier of L is non empty set

R " {a} is Element of bool the carrier of L

(R " {a}) /\ C is Element of bool the carrier of L

L is RelStr

the carrier of L is set

[: the carrier of L, the carrier of L:] is set

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

R is Relation-like the carrier of L -defined the carrier of L -valued auxiliary(i) Element of bool [: the carrier of L, the carrier of L:]

C is set

a is Element of the carrier of L

(L,R,C,a) is Element of bool the carrier of L

bool the carrier of L is non empty set

{a} is non empty trivial 1 -element set

R " {a} is set

(R " {a}) /\ C is set

b is Element of the carrier of L

[b,a] is non empty set

{b,a} is set

{b} is non empty trivial 1 -element set

{{b,a},{b}} is set

L is reflexive transitive RelStr

the carrier of L is set

[: the carrier of L, the carrier of L:] is set

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

bool the carrier of L is non empty set

R is Relation-like the carrier of L -defined the carrier of L -valued auxiliary(ii) Element of bool [: the carrier of L, the carrier of L:]

C is Element of bool the carrier of L

a is Element of the carrier of L

b is Element of the carrier of L

(L,R,C,a) is Element of bool the carrier of L

{a} is non empty trivial 1 -element set

R " {a} is set

(R " {a}) /\ C is set

(L,R,C,b) is Element of bool the carrier of L

{b} is non empty trivial 1 -element set

R " {b} is set

(R " {b}) /\ C is set

d is set

c

the carrier of c

y is Element of the carrier of c

[y,a] is non empty set

{y,a} is set

{y} is non empty trivial 1 -element set

{{y,a},{y}} is set

[y,b] is non empty set

{y,b} is set

{{y,b},{y}} is set

L is RelStr

the carrier of L is set

[: the carrier of L, the carrier of L:] is set

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

R is Relation-like the carrier of L -defined the carrier of L -valued auxiliary(i) Element of bool [: the carrier of L, the carrier of L:]

C is set

a is Element of the carrier of L

[a,a] is non empty set

{a,a} is set

{a} is non empty trivial 1 -element set

{{a,a},{a}} is set

(L,R,C,a) is Element of bool the carrier of L

bool the carrier of L is non empty set

R " {a} is set

(R " {a}) /\ C is set

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

b is Element of the carrier of L

L is RelStr

the carrier of L is set

bool the carrier of L is non empty set

L is non empty reflexive transitive antisymmetric lower-bounded upper-bounded V133() 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 set

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

R is Relation-like the carrier of L -defined the carrier of L -valued transitive auxiliary(i) auxiliary(ii) auxiliary(iv) (L) Element of bool [: the carrier of L, the carrier of L:]

C is (L,R) (L,R)

a is Element of the carrier of L

b is Element of the carrier of L

[b,a] is non empty Element of [: the carrier of L, the carrier of L:]

{b,a} is set

{b} is non empty trivial 1 -element set

{{b,a},{b}} is set

[a,b] is non empty Element of [: the carrier of L, the carrier of L:]

{a,b} is set

{a} is non empty trivial 1 -element set

{{a,b},{a}} is set

d is Element of the carrier of L

[a,d] is non empty Element of [: the carrier of L, the carrier of L:]

{a,d} is set

{{a,d},{a}} is set

[d,b] is non empty Element of [: the carrier of L, the carrier of L:]

{d,b} is set

{d} is non empty trivial 1 -element set

{{d,b},{d}} is set

c

[a,c

{a,c

{{a,c

[c

{c

{c

{{c

(L,R,C,d) is Element of bool the carrier of L

bool the carrier of L is non empty set

R " {d} is set

(R " {d}) /\ C is set

y is non empty set

f is V16() V17() V18() V22() V37() cardinal Element of NAT

f is Element of y

[f,d] is non empty Element of [:y, the carrier of L:]

[:y, the carrier of L:] is non empty set

{f,d} is set

{f} is non empty trivial 1 -element set

{{f,d},{f}} is set

y is Element of the carrier of L

x is Element of the carrier of L

[f,x] is non empty Element of [:y, the carrier of L:]

{f,x} is set

{{f,x},{f}} is set

[x,d] is non empty Element of [: the carrier of L, the carrier of L:]

{x,d} is set

{x} is non empty trivial 1 -element set

{{x,d},{x}} is set

m is Element of y

[f,m] is non empty set

{f,m} is set

{{f,m},{f}} is set

[f,f] is non empty set

{f,f} is set

{{f,f},{f}} is set

y is Element of the carrier of L

[:NAT,y:] is non empty V37() set

bool [:NAT,y:] is non empty V37() set

0 is V16() V17() V18() V22() V37() cardinal Element of NAT

c

f is Relation-like NAT -defined y -valued Function-like V31( NAT ,y) Element of bool [:NAT,y:]

f . 0 is Element of y

[:NAT, the carrier of L:] is non empty V37() set

bool [:NAT, the carrier of L:] is non empty V37() set

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

rng f is Element of bool the carrier of L

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

y is Element of the carrier of L

[y,b] is non empty Element of [: the carrier of L, the carrier of L:]

{y,b} is set

{y} is non empty trivial 1 -element set

{{y,b},{y}} is set

(L,R,C,y) is Element of bool the carrier of L

R " {y} is set

(R " {y}) /\ C is set

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

dom f is Element of bool NAT

x is Element of the carrier of L

m is set

f . m is set

n is V16() V17() V18() V22() V37() cardinal Element of NAT

n + 1 is V16() V17() V18() V22() V37() cardinal Element of NAT

f . (n + 1) is Element of the carrier of L

f . n is Element of the carrier of L

[(f . n),(f . (n + 1))] is non empty Element of [: the carrier of L, the carrier of L:]

{(f . n),(f . (n + 1))} is set

{(f . n)} is non empty trivial 1 -element set

{{(f . n),(f . (n + 1))},{(f . n)}} is set

n is Element of the carrier of L

n is Element of the carrier of L

x is Element of the carrier of L

m is Element of the carrier of L

n is set

f . n is set

n is V16() V17() V18() V22() V37() cardinal Element of NAT

f . n is Element of the carrier of L

k is V16() V17() V18() V22() V37() cardinal set

f . k is set

k + 1 is V16() V17() V18() V22() V37() cardinal Element of NAT

f . (k + 1) is set

f . (k + 1) is Element of the carrier of L

[(f . k),(f . (k + 1))] is non empty set

{(f . k),(f . (k + 1))} is set

{(f . k)} is non empty trivial 1 -element set

{{(f . k),(f . (k + 1))},{(f . k)}} is set

c

f . 0 is set

n + 1 is V16() V17() V18() V22() V37() cardinal Element of NAT

f . (n + 1) is Element of the carrier of L

[(f . n),(f . (n + 1))] is non empty Element of [: the carrier of L, the carrier of L:]

{(f . n),(f . (n + 1))} is set

{(f . n)} is non empty trivial 1 -element set

{{(f . n),(f . (n + 1))},{(f . n)}} is set

[m,y] is non empty Element of [: the carrier of L, the carrier of L:]

{m,y} is set

{m} is non empty trivial 1 -element set

{{m,y},{m}} is set

k is Element of the carrier of L

L is non empty reflexive transitive antisymmetric lower-bounded RelStr

the carrier of L is non empty set

[: the carrier of L, the carrier of L:] is non empty set

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

R is Relation-like the carrier of L -defined the carrier of L -valued auxiliary(i) auxiliary(ii) auxiliary(iv) (L) Element of bool [: the carrier of L, the carrier of L:]

C is non empty (L,R)

a is Element of the carrier of L

(L,R,C,a) is Element of bool the carrier of L

bool the carrier of L is non empty set

{a} is non empty trivial 1 -element set

R " {a} is set

(R " {a}) /\ C is set

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

subrelstr C is non empty strict reflexive transitive antisymmetric V134(L) SubRelStr of L

"\/" ((L,R,C,a),(subrelstr C)) is Element of the carrier of (subrelstr C)

the carrier of (subrelstr C) is non empty set

d is Element of the carrier of L

[a,("\/" ((L,R,C,a),L))] is non empty Element of [: the carrier of L, the carrier of L:]

{a,("\/" ((L,R,C,a),L))} is set

{{a,("\/" ((L,R,C,a),L))},{a}} is set

[("\/" ((L,R,C,a),L)),a] is non empty Element of [: the carrier of L, the carrier of L:]

{("\/" ((L,R,C,a),L)),a} is set

{("\/" ((L,R,C,a),L))} is non empty trivial 1 -element set

{{("\/" ((L,R,C,a),L)),a},{("\/" ((L,R,C,a),L))}} is set

d is Element of the carrier of L

[("\/" ((L,R,C,a),L)),d] is non empty Element of [: the carrier of L, the carrier of L:]

{("\/" ((L,R,C,a),L)),d} is set

{{("\/" ((L,R,C,a),L)),d},{("\/" ((L,R,C,a),L))}} is set

[d,a] is non empty Element of [: the carrier of L, the carrier of L:]

{d,a} is set

{d} is non empty trivial 1 -element set

{{d,a},{d}} is set

L is non empty reflexive antisymmetric RelStr

the carrier of L is non empty set

[: the carrier of L, the carrier of L:] is non empty set

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

R is Relation-like the carrier of L -defined the carrier of L -valued auxiliary(i) Element of bool [: the carrier of L, the carrier of L:]

C is (L,R)

a is Element of the carrier of L

b is Element of the carrier of L

[a,b] is non empty set

{a,b} is set

{a} is non empty trivial 1 -element set

{{a,b},{a}} is set

[a,b] is non empty Element of [: the carrier of L, the carrier of L:]

(L,R,C,b) is Element of bool the carrier of L

bool the carrier of L is non empty set

{b} is non empty trivial 1 -element set

R " {b} is set

(R " {b}) /\ C is set

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

d is Element of the carrier of L

c

[d,c

{d,c

{d} is non empty trivial 1 -element set

{{d,c

[c

{c

{c

{{c

c

d is Element of the carrier of L

d is Element of the carrier of L

[a,d] is non empty set

{a,d} is set

{{a,d},{a}} is set

[d,b] is non empty set

{d,b} is set

{d} is non empty trivial 1 -element set

{{d,b},{d}} is set

[a,d] is non empty Element of [: the carrier of L, the carrier of L:]

[d,b] is non empty Element of [: the carrier of L, 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

[: the carrier of L, the carrier of L:] is non empty set

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

R is Relation-like the carrier of L -defined the carrier of L -valued Element of bool [: the carrier of L, the carrier of L:]

C is set

a is set

b is set

(L,R,C,b) is Element of bool the carrier of L

bool the carrier of L is non empty set

{b} is non empty trivial 1 -element set

R " {b} is set

(R " {b}) /\ C is set

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

d is set

(L,R,C,d) is Element of bool the carrier of L

{d} is non empty trivial 1 -element set

R " {d} is set

(R " {d}) /\ C is set

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

L is non empty RelStr

the carrier of L is non empty set

[: the carrier of L, the carrier of L:] is non empty set

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

R is Relation-like the carrier of L -defined the carrier of L -valued Element of bool [: the carrier of L, the carrier of L:]

C is set

(L,R,C) is set

bool the carrier of L is non empty set

a is set

(L,R,C,a) is Element of bool the carrier of L

{a} is non empty trivial 1 -element set

R " {a} is set

(R " {a}) /\ C is set

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

L is non empty reflexive transitive RelStr

the carrier of L is non empty set

[: the carrier of L, the carrier of L:] is non empty set

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

R is Relation-like the carrier of L -defined the carrier of L -valued auxiliary(i) auxiliary(ii) Element of bool [: the carrier of L, the carrier of L:]

C is (L,R)

(L,R,C) is Element of bool the carrier of L

bool the carrier of L is non empty set

a is set

b is set

[a,b] is non empty set

{a,b} is set

{a} is non empty trivial 1 -element set

{{a,b},{a}} is set

[b,a] is non empty set

{b,a} is set

{b} is non empty trivial 1 -element set

{{b,a},{b}} is set

(L,R,C,a) is Element of bool the carrier of L

R " {a} is set

(R " {a}) /\ C is set

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

d is Element of the carrier of L

(L,R,C,d) is Element of bool the carrier of L

{d} is non empty trivial 1 -element set

R " {d} is set

(R " {d}) /\ C is set

(L,R,C,b) is Element of bool the carrier of L

R " {b} is set

(R " {b}) /\ C is set

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

c

(L,R,C,c

{c

R " {c

(R " {c

y is set

c

[c

{c

{c

{{c

[c

{c

{{c

y is set

c

[c

{c

{c

{{c

[c

{c

{{c

y is Element of the carrier of L

[y,d] is non empty Element of [: the carrier of L, the carrier of L:]

{y,d} is set

{y} is non empty trivial 1 -element set

{{y,d},{y}} is set

[y,c

{y,c

{{y,c

y is Element of the carrier of L

[y,d] is non empty Element of [: the carrier of L, the carrier of L:]

{y,d} is set

{y} is non empty trivial 1 -element set

{{y,d},{y}} is set

[y,c

{y,c

{{y,c

c

[c

{c

{c

{{c

[c

{c

{{c

[y,c

{y,c

{{y,c

c

[c

{c

{c

{{c

[c

{c

{{c

[y,c

{y,c

{{y,c

L is non empty reflexive transitive antisymmetric RelStr

the carrier of L is non empty set

[: the carrier of L, the carrier of L:] is non empty set

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

bool the carrier of L is non empty set

R is Relation-like the carrier of L -defined the carrier of L -valued auxiliary(i) auxiliary(ii) Element of bool [: the carrier of L, the carrier of L:]

C is Element of bool the carrier of L

(L,R,C) is Element of bool the carrier of L

bool (L,R,C) is non empty set

a is Element of bool (L,R,C)

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

subrelstr (L,R,C) is strict reflexive transitive antisymmetric V134(L) SubRelStr of L

"\/" (a,(subrelstr (L,R,C))) is Element of the carrier of (subrelstr (L,R,C))

the carrier of (subrelstr (L,R,C)) is set

(L,R,C,("\/" (a,L))) is Element of bool the carrier of L

{("\/" (a,L))} is non empty trivial 1 -element set

R " {("\/" (a,L))} is set

(R " {("\/" (a,L))}) /\ C is set

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

d is Element of the carrier of L

(L,R,C,d) is Element of bool the carrier of L

{d} is non empty trivial 1 -element set

R " {d} is set

(R " {d}) /\ C is set

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

L is non empty reflexive transitive antisymmetric lower-bounded upper-bounded V133() 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 set

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

R is Relation-like the carrier of L -defined the carrier of L -valued transitive auxiliary(i) auxiliary(ii) auxiliary(iv) (L) Element of bool [: the carrier of L, the carrier of L:]

C is (L,R) (L,R)

(L,R,C) is Element of bool the carrier of L

bool the carrier of L is non empty set

a is Element of the carrier of L

{ b

"\/" ( { b

{ b

"\/" (H

(L,R,C,a) is Element of bool the carrier of L

{a} is non empty trivial 1 -element set

R " {a} is set

(R " {a}) /\ C is set

d is Element of the carrier of L

c

[c

{c

{c

{{c

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

d is Element of the carrier of L

[d,a] is non empty Element of [: the carrier of L, the carrier of L:]

{d,a} is set

{d} is non empty trivial 1 -element set

{{d,a},{d}} is set

d is Element of the carrier of L

d is Element of the carrier of L

d is Element of the carrier of L

[d,a] is non empty Element of [: the carrier of L, the carrier of L:]

{d,a} is set

{d} is non empty trivial 1 -element set

{{d,a},{d}} is set

d is Element of the carrier of L

[d,a] is non empty Element of [: the carrier of L, the carrier of L:]

{d,a} is set

{d} is non empty trivial 1 -element set

{{d,a},{d}} is set

[d,d] is non empty Element of [: the carrier of L, the carrier of L:]

{d,d} is set

{{d,d},{d}} is set

(L,R,C,d) is Element of bool the carrier of L

R " {d} is set

(R " {d}) /\ C is set

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

[d,d] is non empty Element of [: the carrier of L, the carrier of L:]

{d,d} is set

{{d,d},{d}} is set

c

[c

{c

{c

{{c

[c

{c

{{c

[d,c

{d,c

{{d,c

c

c

[c

{c

{c

{{c

c

[c

{c

{c

{{c

y is Element of the carrier of L

[y,c

{y,c

{y} is non empty trivial 1 -element set

{{y,c

(L,R,C,y) is Element of bool the carrier of L

R " {y} is set

(R " {y}) /\ C is set

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

[y,a] is non empty Element of [: the carrier of L, the carrier of L:]

{y,a} is set

{{y,a},{y}} is set

[d,d] is non empty Element of [: the carrier of L, the carrier of L:]

{d,d} is set

{{d,d},{d}} is set

L is non empty reflexive transitive antisymmetric lower-bounded upper-bounded V133() 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 set

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

R is Relation-like the carrier of L -defined the carrier of L -valued transitive auxiliary(i) auxiliary(ii) auxiliary(iv) (L) Element of bool [: the carrier of L, the carrier of L:]

C is (L,R) (L,R)

(L,R,C) is Element of bool the carrier of L

bool the carrier of L is non empty set

a is Element of the carrier of L

b is Element of the carrier of L

[a,b] is non empty set

{a,b} is set

{a} is non empty trivial 1 -element set

{{a,b},{a}} is set

[a,b] is non empty Element of [: the carrier of L, the carrier of L:]

{ b

{ b

"\/" (H

d is Element of the carrier of L

c

[c

{c

{c

{{c

y is Element of the carrier of L

[a,y] is non empty set

{a,y} is set

{{a,y},{a}} is set

[y,b] is non empty set

{y,b} is set

{y} is non empty trivial 1 -element set

{{y,b},{y}} is set

c

(L,R,C,c

{c

R " {c

(R " {c

[a,y] is non empty Element of [: the carrier of L, the carrier of L:]

[y,a] is non empty Element of [: the carrier of L, the carrier of L:]

{y,a} is set

{{y,a},{y}} is set

[y,b] is non empty Element of [: the carrier of L, the carrier of L:]

d is Element of the carrier of L

d is Element of the carrier of L

L is non empty reflexive transitive antisymmetric lower-bounded upper-bounded V133() 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 set

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

R is Relation-like the carrier of L -defined the carrier of L -valued transitive auxiliary(i) auxiliary(ii) auxiliary(iv) (L) Element of bool [: the carrier of L, the carrier of L:]

C is (L,R) (L,R)

(L,R,C) is Element of bool the carrier of L

bool the carrier of L is non empty set

a is Element of the carrier of L

b is Element of the carrier of L

d is Element of the carrier of L

[d,b] is non empty Element of [: the carrier of L, the carrier of L:]

{d,b} is set

{d} is non empty trivial 1 -element set

{{d,b},{d}} is set

(L,R,C,d) is Element of bool the carrier of L

R " {d} is set

(R " {d}) /\ C is set

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