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
{ b1 where b1 is Element of bool the carrier of L : b1 is lower } is set
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
c7 is Element of the carrier of L
y is Element of the carrier of L
c7 is Element of the carrier of L
y is Element of the carrier of L
c7 is Element of the carrier of L
y is Element of the carrier of L
c7 is Element of the carrier of L
y is Element of the carrier of L
c7 is Element of the carrier of L
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
c7 is set
y is set
bool the carrier of L is non empty set
c7 is Element of bool the carrier of L
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
c9 is set
[y,c9] is non empty set
{y,c9} is set
{y} is non empty trivial 1 -element set
{{y,c9},{y}} is set
[c9,y] is non empty set
{c9,y} is set
{c9} is non empty trivial 1 -element set
{{c9,y},{c9}} is set
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
c9 is set
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
c7 is Element of the carrier of L
[d,c7] is non empty Element of [: the carrier of L, the carrier of L:]
{d,c7} is set
{{d,c7},{d}} is set
[c7,d] is non empty Element of [: the carrier of L, the carrier of L:]
{c7,d} is set
{c7} is non empty trivial 1 -element set
{{c7,d},{c7}} is set
[d,c7] is non empty Element of [: the carrier of L, the carrier of L:]
{d,c7} is set
{{d,c7},{d}} is set
[c7,d] is non empty Element of [: the carrier of L, the carrier of L:]
{c7,d} is set
{c7} is non empty trivial 1 -element set
{{c7,d},{c7}} is set
d is set
c7 is set
[d,c7] is non empty set
{d,c7} is set
{d} is non empty trivial 1 -element set
{{d,c7},{d}} is set
[c7,d] is non empty set
{c7,d} is set
{c7} is non empty trivial 1 -element set
{{c7,d},{c7}} is set
y is Element of the carrier of L
c9 is Element of the carrier of L
y is Element of the carrier of L
c9 is Element of the carrier of L
y is Element of the carrier of L
c9 is Element of the carrier of L
y is Element of the carrier of L
c9 is Element of the carrier of L
y is Element of the carrier of L
c9 is Element of the carrier of L
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
c7 is Element of the carrier of (subrelstr C)
y is Element of the carrier of (subrelstr C)
c9 is Element of the carrier of L
y is Element of the carrier of (subrelstr C)
c9 is Element of the carrier of L
[c7,y] is non empty Element of [: the carrier of (subrelstr C), the carrier of (subrelstr C):]
[: the carrier of (subrelstr C), the carrier of (subrelstr C):] is non empty set
{c7,y} is set
{c7} is non empty trivial 1 -element set
{{c7,y},{c7}} is set
[y,c7] is non empty Element of [: the carrier of (subrelstr C), the carrier of (subrelstr C):]
{y,c7} is set
{y} is non empty trivial 1 -element set
{{y,c7},{y}} is 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
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
c7 is Element of the carrier of (subrelstr 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
c9 is Element of the carrier of L
c9 is Element of the carrier of L
c9 is Element of the carrier of L
[("\/" (a,L)),c9] is non empty Element of [: the carrier of L, the carrier of L:]
{("\/" (a,L)),c9} is set
{("\/" (a,L))} is non empty trivial 1 -element set
{{("\/" (a,L)),c9},{("\/" (a,L))}} is set
f is Element of the carrier of L
f is Element of the carrier of L
[f,c9] is non empty Element of [: the carrier of L, the carrier of L:]
{f,c9} is set
{f} is non empty trivial 1 -element set
{{f,c9},{f}} is set
[c9,f] is non empty Element of [: the carrier of L, the carrier of L:]
{c9,f} is set
{c9} is non empty trivial 1 -element set
{{c9,f},{c9}} is set
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
c7 is Element of the carrier of L
c7 is Element of 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
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
c7 is set
y is set
[c7,y] is non empty set
{c7,y} is set
{c7} is non empty trivial 1 -element set
{{c7,y},{c7}} is set
[y,c7] is non empty set
{y,c7} is set
{y} is non empty trivial 1 -element set
{{y,c7},{y}} is set
c9 is Element of the carrier of L
[a,c9] is non empty Element of [: the carrier of L, the carrier of L:]
{a,c9} is set
{{a,c9},{a}} is set
[c9,a] is non empty Element of [: the carrier of L, the carrier of L:]
{c9,a} is set
{c9} is non empty trivial 1 -element set
{{c9,a},{c9}} is set
[c9,b] is non empty Element of [: the carrier of L, the carrier of L:]
{c9,b} is set
{c9} is non empty trivial 1 -element set
{{c9,b},{c9}} is set
[b,c9] is non empty Element of [: the carrier of L, the carrier of L:]
{b,c9} is set
{b} is non empty trivial 1 -element set
{{b,c9},{b}} is set
[a,c9] is non empty Element of [: the carrier of L, the carrier of L:]
{a,c9} is set
{{a,c9},{a}} is set
[c9,b] is non empty Element of [: the carrier of L, the carrier of L:]
{c9,b} is set
{c9} is non empty trivial 1 -element set
{{c9,b},{c9}} is set
c9 is Element of the carrier of L
[a,c9] is non empty Element of [: the carrier of L, the carrier of L:]
{a,c9} is set
{{a,c9},{a}} is set
[c9,a] is non empty Element of [: the carrier of L, the carrier of L:]
{c9,a} is set
{c9} is non empty trivial 1 -element set
{{c9,a},{c9}} is set
[c9,b] is non empty Element of [: the carrier of L, the carrier of L:]
{c9,b} is set
{c9} is non empty trivial 1 -element set
{{c9,b},{c9}} is set
[b,c9] is non empty Element of [: the carrier of L, the carrier of L:]
{b,c9} is set
{b} is non empty trivial 1 -element set
{{b,c9},{b}} is set
[a,c9] is non empty Element of [: the carrier of L, the carrier of L:]
{a,c9} is set
{{a,c9},{a}} is set
[c9,b] is non empty Element of [: the carrier of L, the carrier of L:]
{c9,b} is set
{c9} is non empty trivial 1 -element set
{{c9,b},{c9}} is set
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
c7 is non empty reflexive RelStr
the carrier of c7 is non empty set
y is Element of the carrier of c7
[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
c7 is Element of the carrier of L
[a,c7] is non empty Element of [: the carrier of L, the carrier of L:]
{a,c7} is set
{{a,c7},{a}} is set
[c7,d] is non empty Element of [: the carrier of L, the carrier of L:]
{c7,d} is set
{c7} is non empty trivial 1 -element set
{{c7,d},{c7}} is set
(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
c9 is Element of y
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
c18 is Element of the carrier of L
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
c7 is Element of the carrier of L
[d,c7] is non empty Element of [: the carrier of L, the carrier of L:]
{d,c7} is set
{d} is non empty trivial 1 -element set
{{d,c7},{d}} is set
[c7,d] is non empty Element of [: the carrier of L, the carrier of L:]
{c7,d} is set
{c7} is non empty trivial 1 -element set
{{c7,d},{c7}} is set
c7 is Element of the carrier of L
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
c7 is Element of the carrier of L
(L,R,C,c7) is Element of bool the carrier of L
{c7} is non empty trivial 1 -element set
R " {c7} is set
(R " {c7}) /\ C is set
y is set
c9 is Element of the carrier of L
[c9,d] is non empty Element of [: the carrier of L, the carrier of L:]
{c9,d} is set
{c9} is non empty trivial 1 -element set
{{c9,d},{c9}} is set
[c9,c7] is non empty Element of [: the carrier of L, the carrier of L:]
{c9,c7} is set
{{c9,c7},{c9}} is set
y is set
c9 is Element of the carrier of L
[c9,c7] is non empty Element of [: the carrier of L, the carrier of L:]
{c9,c7} is set
{c9} is non empty trivial 1 -element set
{{c9,c7},{c9}} is set
[c9,d] is non empty Element of [: the carrier of L, the carrier of L:]
{c9,d} is set
{{c9,d},{c9}} is set
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,c7] is non empty Element of [: the carrier of L, the carrier of L:]
{y,c7} is set
{{y,c7},{y}} is set
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,c7] is non empty Element of [: the carrier of L, the carrier of L:]
{y,c7} is set
{{y,c7},{y}} is set
c9 is Element of the carrier of L
[c9,c7] is non empty Element of [: the carrier of L, the carrier of L:]
{c9,c7} is set
{c9} is non empty trivial 1 -element set
{{c9,c7},{c9}} is set
[c9,y] is non empty Element of [: the carrier of L, the carrier of L:]
{c9,y} is set
{{c9,y},{c9}} is set
[y,c9] is non empty Element of [: the carrier of L, the carrier of L:]
{y,c9} is set
{{y,c9},{y}} is set
c9 is Element of the carrier of L
[c9,d] is non empty Element of [: the carrier of L, the carrier of L:]
{c9,d} is set
{c9} is non empty trivial 1 -element set
{{c9,d},{c9}} is set
[c9,y] is non empty Element of [: the carrier of L, the carrier of L:]
{c9,y} is set
{{c9,y},{c9}} is set
[y,c9] is non empty Element of [: the carrier of L, the carrier of L:]
{y,c9} is set
{{y,c9},{y}} is 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
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
{ b1 where b1 is Element of the carrier of L : ( b1 in (L,R,C) & [b1,a] in R ) } is set
"\/" ( { b1 where b1 is Element of the carrier of L : ( b1 in (L,R,C) & [b1,a] in R ) } ,L) is Element of the carrier of L
{ b1 where b1 is Element of the carrier of L : ( b1 in (L,R,C) & [b1,a1] in R ) } is set
"\/" (H1(a),L) 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
d is Element of the carrier of L
c7 is Element of the carrier of L
[c7,a] is non empty Element of [: the carrier of L, the carrier of L:]
{c7,a} is set
{c7} is non empty trivial 1 -element set
{{c7,a},{c7}} is set
"\/" ((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
c7 is Element of the carrier of L
[c7,a] is non empty Element of [: the carrier of L, the carrier of L:]
{c7,a} is set
{c7} is non empty trivial 1 -element set
{{c7,a},{c7}} is set
[c7,d] is non empty Element of [: the carrier of L, the carrier of L:]
{c7,d} is set
{{c7,d},{c7}} is set
[d,c7] is non empty Element of [: the carrier of L, the carrier of L:]
{d,c7} is set
{{d,c7},{d}} is set
c7 is Element of the carrier of L
c7 is Element of the carrier of L
[c7,a] is non empty Element of [: the carrier of L, the carrier of L:]
{c7,a} is set
{c7} is non empty trivial 1 -element set
{{c7,a},{c7}} is set
c7 is Element of the carrier of L
[c7,a] is non empty Element of [: the carrier of L, the carrier of L:]
{c7,a} is set
{c7} is non empty trivial 1 -element set
{{c7,a},{c7}} is set
y is Element of the carrier of L
[y,c7] is non empty Element of [: the carrier of L, the carrier of L:]
{y,c7} is set
{y} is non empty trivial 1 -element set
{{y,c7},{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
[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:]
{ b1 where b1 is Element of the carrier of L : ( b1 in (L,R,C) & [b1,a1] in R ) } is set
{ b1 where b1 is Element of the carrier of L : ( b1 in (L,R,C) & [b1,b] in R ) } is set
"\/" (H1(b),L) is Element of the carrier of L
d is Element of the carrier of L
c7 is Element of the carrier of L
[c7,b] is non empty Element of [: the carrier of L, the carrier of L:]
{c7,b} is set
{c7} is non empty trivial 1 -element set
{{c7,b},{c7}} is set
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
c9 is Element of the carrier of L
(L,R,C,c9) is Element of bool the carrier of L
{c9} is non empty trivial 1 -element set
R " {c9} is set
(R " {c9}) /\ C is set
[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