:: INTERVA1 semantic presentation

K173() is Element of K19(K169())
K169() is set
K19(K169()) is non empty set
K88() is set
K19(K88()) is non empty set
K19(K173()) is non empty set
{} is empty set
the empty set is empty set
1 is non empty set
X is set
K19(X) is non empty set
Y is Element of K19(X)
A1 is Element of K19(X)
{ b₁ where b₁ is Element of K19(X) : ( Y c= b₁ & b₁ c= A1 ) } is set
K19(K19(X)) is non empty set
bool X is non empty Element of K19(K19(X))
a9 is set
f is Element of K19(X)
X is set
K19(X) is non empty set
Y is Element of K19(X)
A1 is Element of K19(X)
(X,Y,A1) is Element of K19(K19(X))
K19(K19(X)) is non empty set
{ b₁ where b₁ is Element of K19(X) : ( Y c= b₁ & b₁ c= A1 ) } is set
A2 is set
bool X is non empty Element of K19(K19(X))
a9 is Element of bool X
X is set
K19(X) is non empty set
Y is Element of K19(X)
A1 is Element of K19(X)
(X,Y,A1) is Element of K19(K19(X))
K19(K19(X)) is non empty set
{ b₁ where b₁ is Element of K19(X) : ( Y c= b₁ & b₁ c= A1 ) } is set
A2 is set
X is set
K19(X) is non empty set
Y is Element of K19(X)
A1 is Element of K19(X)
(X,Y,A1) is Element of K19(K19(X))
K19(K19(X)) is non empty set
{ b₁ where b₁ is Element of K19(X) : ( Y c= b₁ & b₁ c= A1 ) } is set
A2 is set
X is set
K19(X) is non empty set
Y is Element of K19(X)
A1 is Element of K19(X)
(X,Y,A1) is Element of K19(K19(X))
K19(K19(X)) is non empty set
{ b₁ where b₁ is Element of K19(X) : ( Y c= b₁ & b₁ c= A1 ) } is set
X is set
K19(X) is non empty set
Y is Element of K19(X)
A1 is Element of K19(X)
(X,Y,A1) is Element of K19(K19(X))
K19(K19(X)) is non empty set
{ b₁ where b₁ is Element of K19(X) : ( Y c= b₁ & b₁ c= A1 ) } is set
A2 is set
X is set
K19(X) is non empty set
Y is Element of K19(X)
A1 is Element of K19(X)
(X,Y,A1) is Element of K19(K19(X))
K19(K19(X)) is non empty set
{ b₁ where b₁ is Element of K19(X) : ( Y c= b₁ & b₁ c= A1 ) } is set
A2 is Element of K19(X)
a9 is Element of K19(X)
(X,A2,a9) is Element of K19(K19(X))
{ b₁ where b₁ is Element of K19(X) : ( A2 c= b₁ & b₁ c= a9 ) } is set
X is non empty set
K19(X) is non empty set
{} X is empty proper Element of K19(X)
Y is non empty Element of K19(X)
(X,Y,({} X)) is Element of K19(K19(X))
K19(K19(X)) is non empty set
{ b₁ where b₁ is Element of K19(X) : ( Y c= b₁ & b₁ c= {} X ) } is set
A1 is set
X is set
K19(X) is non empty set
Y is Element of K19(X)
(X,Y,Y) is Element of K19(K19(X))
K19(K19(X)) is non empty set
{ b₁ where b₁ is Element of K19(X) : ( Y c= b₁ & b₁ c= Y ) } is set
{Y} is non empty set
A1 is set
A1 is set
X is set
K19(X) is non empty set
K19(K19(X)) is non empty set
the Element of K19(X) is Element of K19(X)
{ the Element of K19(X)} is non empty set
(X, the Element of K19(X), the Element of K19(X)) is Element of K19(K19(X))
{ b₁ where b₁ is Element of K19(X) : ( the Element of K19(X) c= b₁ & b₁ c= the Element of K19(X) ) } is set
X is non empty set
K19(X) is non empty set
the non empty Element of K19(X) is non empty Element of K19(X)
{} X is empty proper Element of K19(X)
(X, the non empty Element of K19(X),({} X)) is Element of K19(K19(X))
K19(K19(X)) is non empty set
{ b₁ where b₁ is Element of K19(X) : ( the non empty Element of K19(X) c= b₁ & b₁ c= {} X ) } is set
X is non empty set
K19(X) is non empty set
Y is Element of K19(X)
{Y} is non empty set
(X,Y,Y) is Element of K19(K19(X))
K19(K19(X)) is non empty set
{ b₁ where b₁ is Element of K19(X) : ( Y c= b₁ & b₁ c= Y ) } is set
X is set
K19(X) is non empty set
Y is Element of K19(X)
A1 is Element of K19(X)
(X,Y,A1) is Element of K19(K19(X))
K19(K19(X)) is non empty set
{ b₁ where b₁ is Element of K19(X) : ( Y c= b₁ & b₁ c= A1 ) } is set
X is non empty set
K19(X) is non empty set
the Element of K19(X) is Element of K19(X)
{ the Element of K19(X)} is non empty set
X is non empty set
K19(X) is non empty set
Y is set
A1 is Element of K19(X)
A2 is Element of K19(X)
(X,A1,A2) is (X)
{ b₁ where b₁ is Element of K19(X) : ( A1 c= b₁ & b₁ c= A2 ) } is set
a9 is Element of K19(X)
f is Element of K19(X)
(X,a9,f) is (X)
{ b₁ where b₁ is Element of K19(X) : ( a9 c= b₁ & b₁ c= f ) } is set
A1 is Element of K19(X)
A2 is Element of K19(X)
(X,A1,A2) is (X)
{ b₁ where b₁ is Element of K19(X) : ( A1 c= b₁ & b₁ c= A2 ) } is set
X is non empty set
K19(X) is non empty set
Y is Element of K19(X)
A1 is Element of K19(X)
A2 is Element of K19(X)
a9 is Element of K19(X)
(X,Y,A1) is (X)
{ b₁ where b₁ is Element of K19(X) : ( Y c= b₁ & b₁ c= A1 ) } is set
(X,A2,a9) is (X)
{ b₁ where b₁ is Element of K19(X) : ( A2 c= b₁ & b₁ c= a9 ) } is set
INTERSECTION ((X,Y,A1),(X,A2,a9)) is set
Y /\ A2 is Element of K19(X)
A1 /\ a9 is Element of K19(X)
{ b₁ where b₁ is Element of K19(X) : ( Y /\ A2 c= b₁ & b₁ c= A1 /\ a9 ) } is set
a is set
b is set
b9 is set
b /\ b9 is set
a is set
b is Element of K19(X)
a \/ Y is set
(a \/ Y) /\ A1 is Element of K19(X)
a \/ A2 is set
(a \/ A2) /\ a9 is Element of K19(X)
(Y /\ A2) \/ a is set
(A1 /\ a9) /\ a is Element of K19(X)
((a \/ Y) /\ A1) /\ ((a \/ A2) /\ a9) is Element of K19(X)
A1 /\ ((a \/ A2) /\ a9) is Element of K19(X)
(a \/ Y) /\ (A1 /\ ((a \/ A2) /\ a9)) is Element of K19(X)
a9 /\ A1 is Element of K19(X)
(a \/ A2) /\ (a9 /\ A1) is Element of K19(X)
(a \/ Y) /\ ((a \/ A2) /\ (a9 /\ A1)) is Element of K19(X)
(a \/ Y) /\ (a \/ A2) is set
((a \/ Y) /\ (a \/ A2)) /\ (A1 /\ a9) is Element of K19(X)
Y /\ A1 is Element of K19(X)
a /\ A1 is Element of K19(X)
(a /\ A1) \/ Y is Element of K19(X)
A2 /\ a9 is Element of K19(X)
a /\ a9 is Element of K19(X)
(a /\ a9) \/ A2 is Element of K19(X)
X is non empty set
K19(X) is non empty set
Y is Element of K19(X)
A1 is Element of K19(X)
A2 is Element of K19(X)
a9 is Element of K19(X)
(X,Y,A1) is (X)
{ b₁ where b₁ is Element of K19(X) : ( Y c= b₁ & b₁ c= A1 ) } is set
(X,A2,a9) is (X)
{ b₁ where b₁ is Element of K19(X) : ( A2 c= b₁ & b₁ c= a9 ) } is set
UNION ((X,Y,A1),(X,A2,a9)) is set
Y \/ A2 is Element of K19(X)
A1 \/ a9 is Element of K19(X)
{ b₁ where b₁ is Element of K19(X) : ( Y \/ A2 c= b₁ & b₁ c= A1 \/ a9 ) } is set
a is set
b is set
b9 is set
b \/ b9 is set
a is set
b is Element of K19(X)
a \/ Y is set
(a \/ Y) /\ A1 is Element of K19(X)
a \/ A2 is set
(a \/ A2) /\ a9 is Element of K19(X)
(Y \/ A2) \/ a is set
(A1 \/ a9) /\ a is Element of K19(X)
Y /\ A1 is Element of K19(X)
A2 /\ a9 is Element of K19(X)
((a \/ Y) /\ A1) \/ ((a \/ A2) /\ a9) is Element of K19(X)
a /\ A1 is Element of K19(X)
(a /\ A1) \/ (Y /\ A1) is Element of K19(X)
((a /\ A1) \/ (Y /\ A1)) \/ ((a \/ A2) /\ a9) is Element of K19(X)
(a /\ A1) \/ Y is Element of K19(X)
a /\ a9 is Element of K19(X)
(a /\ a9) \/ (A2 /\ a9) is Element of K19(X)
((a /\ A1) \/ Y) \/ ((a /\ a9) \/ (A2 /\ a9)) is Element of K19(X)
(a /\ a9) \/ A2 is Element of K19(X)
Y \/ ((a /\ a9) \/ A2) is Element of K19(X)
(a /\ A1) \/ (Y \/ ((a /\ a9) \/ A2)) is Element of K19(X)
(a /\ a9) \/ (Y \/ A2) is Element of K19(X)
(a /\ A1) \/ ((a /\ a9) \/ (Y \/ A2)) is Element of K19(X)
(a /\ A1) \/ (a /\ a9) is Element of K19(X)
((a /\ A1) \/ (a /\ a9)) \/ (Y \/ A2) is Element of K19(X)
X is non empty set
Y is non empty (X)
A1 is non empty (X)
INTERSECTION (Y,A1) is set
K19(X) is non empty set
a9 is Element of K19(X)
f is Element of K19(X)
(X,a9,f) is (X)
{ b₁ where b₁ is Element of K19(X) : ( a9 c= b₁ & b₁ c= f ) } is set
f is Element of K19(X)
g is Element of K19(X)
(X,f,g) is (X)
{ b₁ where b₁ is Element of K19(X) : ( f c= b₁ & b₁ c= g ) } is set
a9 /\ f is Element of K19(X)
f /\ g is Element of K19(X)
(X,(a9 /\ f),(f /\ g)) is (X)
{ b₁ where b₁ is Element of K19(X) : ( a9 /\ f c= b₁ & b₁ c= f /\ g ) } is set
UNION (Y,A1) is set
K19(X) is non empty set
a9 is Element of K19(X)
f is Element of K19(X)
(X,a9,f) is (X)
{ b₁ where b₁ is Element of K19(X) : ( a9 c= b₁ & b₁ c= f ) } is set
f is Element of K19(X)
g is Element of K19(X)
(X,f,g) is (X)
{ b₁ where b₁ is Element of K19(X) : ( f c= b₁ & b₁ c= g ) } is set
a9 \/ f is Element of K19(X)
f \/ g is Element of K19(X)
(X,(a9 \/ f),(f \/ g)) is (X)
{ b₁ where b₁ is Element of K19(X) : ( a9 \/ f c= b₁ & b₁ c= f \/ g ) } is set
X is non empty set
Y is non empty (X)
A1 is non empty (X)
(X,Y,A1) is (X)
INTERSECTION (Y,A1) is set
(X,Y,A1) is (X)
UNION (Y,A1) is set
X is non empty set
K19(X) is non empty set
Y is non empty (X)
A1 is Element of K19(X)
A2 is Element of K19(X)
(X,A1,A2) is (X)
{ b₁ where b₁ is Element of K19(X) : ( A1 c= b₁ & b₁ c= A2 ) } is set
A1 is Element of K19(X)
a9 is Element of K19(X)
(X,A1,a9) is (X)
{ b₁ where b₁ is Element of K19(X) : ( A1 c= b₁ & b₁ c= a9 ) } is set
A2 is Element of K19(X)
f is Element of K19(X)
(X,A2,f) is (X)
{ b₁ where b₁ is Element of K19(X) : ( A2 c= b₁ & b₁ c= f ) } is set
A1 is Element of K19(X)
A2 is Element of K19(X)
(X,A1,A2) is (X)
{ b₁ where b₁ is Element of K19(X) : ( A1 c= b₁ & b₁ c= A2 ) } is set
a9 is Element of K19(X)
A1 is Element of K19(X)
(X,a9,A1) is (X)
{ b₁ where b₁ is Element of K19(X) : ( a9 c= b₁ & b₁ c= A1 ) } is set
f is Element of K19(X)
A2 is Element of K19(X)
(X,f,A2) is (X)
{ b₁ where b₁ is Element of K19(X) : ( f c= b₁ & b₁ c= A2 ) } is set
X is non empty set
Y is non empty (X)
(X,Y) is Element of K19(X)
K19(X) is non empty set
(X,Y) is Element of K19(X)
A1 is set
A2 is Element of K19(X)
(X,(X,Y),A2) is (X)
{ b₁ where b₁ is Element of K19(X) : ( (X,Y) c= b₁ & b₁ c= A2 ) } is set
A2 is Element of K19(X)
(X,A2,(X,Y)) is (X)
{ b₁ where b₁ is Element of K19(X) : ( A2 c= b₁ & b₁ c= (X,Y) ) } is set
(X,(X,Y),(X,Y)) is (X)
{ b₁ where b₁ is Element of K19(X) : ( (X,Y) c= b₁ & b₁ c= (X,Y) ) } is set
A2 is Element of K19(X)
(X,(X,Y),A2) is (X)
{ b₁ where b₁ is Element of K19(X) : ( (X,Y) c= b₁ & b₁ c= A2 ) } is set
a9 is Element of K19(X)
(X,a9,(X,Y)) is (X)
{ b₁ where b₁ is Element of K19(X) : ( a9 c= b₁ & b₁ c= (X,Y) ) } is set
X is non empty set
Y is non empty (X)
(X,Y) is Element of K19(X)
K19(X) is non empty set
(X,Y) is Element of K19(X)
(X,(X,Y),(X,Y)) is (X)
{ b₁ where b₁ is Element of K19(X) : ( (X,Y) c= b₁ & b₁ c= (X,Y) ) } is set
A1 is set
A1 is set
X is non empty set
Y is non empty (X)
(X,Y) is Element of K19(X)
K19(X) is non empty set
(X,Y) is Element of K19(X)
A1 is Element of K19(X)
(X,(X,Y),A1) is (X)
{ b₁ where b₁ is Element of K19(X) : ( (X,Y) c= b₁ & b₁ c= A1 ) } is set
A2 is Element of K19(X)
(X,A2,(X,Y)) is (X)
{ b₁ where b₁ is Element of K19(X) : ( A2 c= b₁ & b₁ c= (X,Y) ) } is set
X is non empty set
Y is non empty (X)
(X,Y) is Element of K19(X)
K19(X) is non empty set
(X,Y) is Element of K19(X)
A1 is non empty (X)
(X,Y,A1) is non empty (X)
UNION (Y,A1) is set
(X,A1) is Element of K19(X)
(X,Y) \/ (X,A1) is Element of K19(X)
(X,A1) is Element of K19(X)
(X,Y) \/ (X,A1) is Element of K19(X)
(X,((X,Y) \/ (X,A1)),((X,Y) \/ (X,A1))) is (X)
{ b₁ where b₁ is Element of K19(X) : ( (X,Y) \/ (X,A1) c= b₁ & b₁ c= (X,Y) \/ (X,A1) ) } is set
A2 is set
a9 is set
f is set
a9 \/ f is set
A2 is set
bool X is non empty Element of K19(K19(X))
K19(K19(X)) is non empty set
a9 is Element of bool X
a9 \/ (X,Y) is Element of K19(X)
(a9 \/ (X,Y)) /\ (X,Y) is Element of K19(X)
f is set
a9 \/ (X,A1) is Element of K19(X)
(a9 \/ (X,A1)) /\ (X,A1) is Element of K19(X)
f is set
((a9 \/ (X,Y)) /\ (X,Y)) \/ ((a9 \/ (X,A1)) /\ (X,A1)) is Element of K19(X)
((a9 \/ (X,Y)) /\ (X,Y)) \/ (a9 \/ (X,A1)) is Element of K19(X)
((a9 \/ (X,Y)) /\ (X,Y)) \/ (X,A1) is Element of K19(X)
(((a9 \/ (X,Y)) /\ (X,Y)) \/ (a9 \/ (X,A1))) /\ (((a9 \/ (X,Y)) /\ (X,Y)) \/ (X,A1)) is Element of K19(X)
(a9 \/ (X,Y)) \/ (a9 \/ (X,A1)) is Element of K19(X)
(X,Y) \/ (a9 \/ (X,A1)) is Element of K19(X)
((a9 \/ (X,Y)) \/ (a9 \/ (X,A1))) /\ ((X,Y) \/ (a9 \/ (X,A1))) is Element of K19(X)
(((a9 \/ (X,Y)) \/ (a9 \/ (X,A1))) /\ ((X,Y) \/ (a9 \/ (X,A1)))) /\ (((a9 \/ (X,Y)) /\ (X,Y)) \/ (X,A1)) is Element of K19(X)
a9 \/ ((X,Y) \/ (X,A1)) is Element of K19(X)
(a9 \/ ((X,Y) \/ (X,A1))) /\ ((X,Y) \/ (a9 \/ (X,A1))) is Element of K19(X)
((a9 \/ ((X,Y) \/ (X,A1))) /\ ((X,Y) \/ (a9 \/ (X,A1)))) /\ (((a9 \/ (X,Y)) /\ (X,Y)) \/ (X,A1)) is Element of K19(X)
a9 /\ ((X,Y) \/ (a9 \/ (X,A1))) is Element of K19(X)
(a9 /\ ((X,Y) \/ (a9 \/ (X,A1)))) /\ (((a9 \/ (X,Y)) /\ (X,Y)) \/ (X,A1)) is Element of K19(X)
a9 /\ (X,Y) is Element of K19(X)
a9 /\ (a9 \/ (X,A1)) is Element of K19(X)
(a9 /\ (X,Y)) \/ (a9 /\ (a9 \/ (X,A1))) is Element of K19(X)
((a9 /\ (X,Y)) \/ (a9 /\ (a9 \/ (X,A1)))) /\ (((a9 \/ (X,Y)) /\ (X,Y)) \/ (X,A1)) is Element of K19(X)
(a9 /\ (X,Y)) \/ a9 is Element of K19(X)
((a9 /\ (X,Y)) \/ a9) /\ (((a9 \/ (X,Y)) /\ (X,Y)) \/ (X,A1)) is Element of K19(X)
(X,A1) \/ ((a9 \/ (X,Y)) /\ (X,Y)) is Element of K19(X)
a9 /\ ((X,A1) \/ ((a9 \/ (X,Y)) /\ (X,Y))) is Element of K19(X)
(a9 \/ (X,Y)) \/ (X,A1) is Element of K19(X)
((a9 \/ (X,Y)) \/ (X,A1)) /\ ((X,Y) \/ (X,A1)) is Element of K19(X)
a9 /\ (((a9 \/ (X,Y)) \/ (X,A1)) /\ ((X,Y) \/ (X,A1))) is Element of K19(X)
(X,Y) \/ (X,A1) is Element of K19(X)
a9 \/ ((X,Y) \/ (X,A1)) is Element of K19(X)
(a9 \/ ((X,Y) \/ (X,A1))) /\ ((X,Y) \/ (X,A1)) is Element of K19(X)
a9 /\ ((a9 \/ ((X,Y) \/ (X,A1))) /\ ((X,Y) \/ (X,A1))) is Element of K19(X)
a9 /\ ((X,Y) \/ (X,A1)) is Element of K19(X)
((X,Y) \/ (X,A1)) /\ ((X,Y) \/ (X,A1)) is Element of K19(X)
(a9 /\ ((X,Y) \/ (X,A1))) \/ (((X,Y) \/ (X,A1)) /\ ((X,Y) \/ (X,A1))) is Element of K19(X)
a9 /\ ((a9 /\ ((X,Y) \/ (X,A1))) \/ (((X,Y) \/ (X,A1)) /\ ((X,Y) \/ (X,A1)))) is Element of K19(X)
a9 \/ (((X,Y) \/ (X,A1)) /\ ((X,Y) \/ (X,A1))) is Element of K19(X)
a9 /\ (a9 \/ (((X,Y) \/ (X,A1)) /\ ((X,Y) \/ (X,A1)))) is Element of K19(X)
a9 \/ ((X,Y) \/ (X,A1)) is Element of K19(X)
(a9 \/ ((X,Y) \/ (X,A1))) /\ (a9 \/ ((X,Y) \/ (X,A1))) is Element of K19(X)
a9 /\ ((a9 \/ ((X,Y) \/ (X,A1))) /\ (a9 \/ ((X,Y) \/ (X,A1)))) is Element of K19(X)
a9 /\ (a9 \/ ((X,Y) \/ (X,A1))) is Element of K19(X)
(a9 /\ (a9 \/ ((X,Y) \/ (X,A1)))) /\ (a9 \/ ((X,Y) \/ (X,A1))) is Element of K19(X)
a9 /\ (a9 \/ ((X,Y) \/ (X,A1))) is Element of K19(X)
f is Element of K19(X)
f is Element of K19(X)
f \/ f is Element of K19(X)
X is non empty set
Y is non empty (X)
(X,Y) is Element of K19(X)
K19(X) is non empty set
(X,Y) is Element of K19(X)
A1 is non empty (X)
(X,Y,A1) is non empty (X)
INTERSECTION (Y,A1) is set
(X,A1) is Element of K19(X)
(X,Y) /\ (X,A1) is Element of K19(X)
(X,A1) is Element of K19(X)
(X,Y) /\ (X,A1) is Element of K19(X)
(X,((X,Y) /\ (X,A1)),((X,Y) /\ (X,A1))) is (X)
{ b₁ where b₁ is Element of K19(X) : ( (X,Y) /\ (X,A1) c= b₁ & b₁ c= (X,Y) /\ (X,A1) ) } is set
A2 is set
a9 is set
f is set
a9 /\ f is set
A2 is set
bool X is non empty Element of K19(K19(X))
K19(K19(X)) is non empty set
a9 is Element of bool X
a9 \/ (X,Y) is Element of K19(X)
(a9 \/ (X,Y)) /\ (X,Y) is Element of K19(X)
f is set
a9 \/ (X,A1) is Element of K19(X)
(a9 \/ (X,A1)) /\ (X,A1) is Element of K19(X)
f is set
((a9 \/ (X,Y)) /\ (X,Y)) /\ ((a9 \/ (X,A1)) /\ (X,A1)) is Element of K19(X)
(X,Y) /\ (a9 \/ (X,Y)) is Element of K19(X)
((X,Y) /\ (a9 \/ (X,Y))) /\ (a9 \/ (X,A1)) is Element of K19(X)
(((X,Y) /\ (a9 \/ (X,Y))) /\ (a9 \/ (X,A1))) /\ (X,A1) is Element of K19(X)
(a9 \/ (X,Y)) /\ (a9 \/ (X,A1)) is Element of K19(X)
(X,Y) /\ ((a9 \/ (X,Y)) /\ (a9 \/ (X,A1))) is Element of K19(X)
((X,Y) /\ ((a9 \/ (X,Y)) /\ (a9 \/ (X,A1)))) /\ (X,A1) is Element of K19(X)
a9 \/ ((X,Y) /\ (X,A1)) is Element of K19(X)
(X,Y) /\ (a9 \/ ((X,Y) /\ (X,A1))) is Element of K19(X)
((X,Y) /\ (a9 \/ ((X,Y) /\ (X,A1)))) /\ (X,A1) is Element of K19(X)
(X,Y) /\ a9 is Element of K19(X)
((X,Y) /\ a9) /\ (X,A1) is Element of K19(X)
a9 /\ ((X,Y) /\ (X,A1)) is Element of K19(X)
X is non empty set
Y is non empty (X)
A1 is non empty (X)
(X,Y) is Element of K19(X)
K19(X) is non empty set
(X,A1) is Element of K19(X)
(X,Y) is Element of K19(X)
(X,A1) is Element of K19(X)
A2 is set
a9 is Element of K19(X)
f is Element of K19(X)
(X,a9,f) is (X)
{ b₁ where b₁ is Element of K19(X) : ( a9 c= b₁ & b₁ c= f ) } is set
f is Element of K19(X)
(X,(X,Y),f) is (X)
{ b₁ where b₁ is Element of K19(X) : ( (X,Y) c= b₁ & b₁ c= f ) } is set
g is Element of K19(X)
(X,(X,A1),g) is (X)
{ b₁ where b₁ is Element of K19(X) : ( (X,A1) c= b₁ & b₁ c= g ) } is set
g is Element of K19(X)
(X,g,(X,Y)) is (X)
{ b₁ where b₁ is Element of K19(X) : ( g c= b₁ & b₁ c= (X,Y) ) } is set
a9 is Element of K19(X)
(X,a9,(X,A1)) is (X)
{ b₁ where b₁ is Element of K19(X) : ( a9 c= b₁ & b₁ c= (X,A1) ) } is set
A2 is set
a9 is Element of K19(X)
f is Element of K19(X)
(X,a9,f) is (X)
{ b₁ where b₁ is Element of K19(X) : ( a9 c= b₁ & b₁ c= f ) } is set
f is Element of K19(X)
(X,(X,A1),f) is (X)
{ b₁ where b₁ is Element of K19(X) : ( (X,A1) c= b₁ & b₁ c= f ) } is set
g is Element of K19(X)
(X,(X,Y),g) is (X)
{ b₁ where b₁ is Element of K19(X) : ( (X,Y) c= b₁ & b₁ c= g ) } is set
g is Element of K19(X)
(X,g,(X,A1)) is (X)
{ b₁ where b₁ is Element of K19(X) : ( g c= b₁ & b₁ c= (X,A1) ) } is set
a9 is Element of K19(X)
(X,a9,(X,Y)) is (X)
{ b₁ where b₁ is Element of K19(X) : ( a9 c= b₁ & b₁ c= (X,Y) ) } is set
X is non empty set
Y is non empty (X)
(X,Y,Y) is non empty (X)
UNION (Y,Y) is set
A1 is set
A2 is set
a9 is set
A2 \/ a9 is set
(X,Y) is Element of K19(X)
K19(X) is non empty set
(X,Y) is Element of K19(X)
A1 is set
A1 \/ A1 is set
X is non empty set
Y is non empty (X)
(X,Y,Y) is non empty (X)
INTERSECTION (Y,Y) is set
A1 is set
A2 is set
a9 is set
A2 /\ a9 is set
(X,Y) is Element of K19(X)
K19(X) is non empty set
(X,Y) is Element of K19(X)
A1 is set
A1 /\ A1 is set
X is non empty set
Y is non empty (X)
A1 is non empty (X)
(X,Y,A1) is non empty (X)
UNION (Y,A1) is set
(X,A1,Y) is non empty (X)
UNION (A1,Y) is set
X is non empty set
Y is non empty (X)
A1 is non empty (X)
(X,Y,A1) is non empty (X)
INTERSECTION (Y,A1) is set
(X,A1,Y) is non empty (X)
INTERSECTION (A1,Y) is set
X is non empty set
Y is non empty (X)
A1 is non empty (X)
(X,Y,A1) is non empty (X)
UNION (Y,A1) is set
A2 is non empty (X)
(X,(X,Y,A1),A2) is non empty (X)
UNION ((X,Y,A1),A2) is set
(X,A1,A2) is non empty (X)
UNION (A1,A2) is set
(X,Y,(X,A1,A2)) is non empty (X)
UNION (Y,(X,A1,A2)) is set
a9 is set
f is set
f is set
f \/ f is set
g is set
g is set
g \/ g is set
g \/ f is set
g \/ (g \/ f) is set
UNION (Y,(UNION (A1,A2))) is set
a9 is set
f is set
f is set
f \/ f is set
g is set
g is set
g \/ g is set
f \/ g is set
(f \/ g) \/ g is set
UNION ((UNION (Y,A1)),A2) is set
X is non empty set
Y is non empty (X)
A1 is non empty (X)
(X,Y,A1) is non empty (X)
INTERSECTION (Y,A1) is set
A2 is non empty (X)
(X,(X,Y,A1),A2) is non empty (X)
INTERSECTION ((X,Y,A1),A2) is set
(X,A1,A2) is non empty (X)
INTERSECTION (A1,A2) is set
(X,Y,(X,A1,A2)) is non empty (X)
INTERSECTION (Y,(X,A1,A2)) is set
a9 is set
f is set
f is set
f /\ f is set
g is set
g is set
g /\ g is set
g /\ f is set
g /\ (g /\ f) is set
INTERSECTION (Y,(INTERSECTION (A1,A2))) is set
a9 is set
f is set
f is set
f /\ f is set
g is set
g is set
g /\ g is set
f /\ g is set
(f /\ g) /\ g is set
INTERSECTION ((INTERSECTION (Y,A1)),A2) is set
X is set
K19(X) is non empty set
K19(K19(X)) is non empty set
Y is Element of K19(K19(X))
A1 is Element of K19(K19(X))
A2 is Element of K19(K19(X))
INTERSECTION (A1,A2) is set
UNION (Y,(INTERSECTION (A1,A2))) is set
UNION (Y,A1) is set
UNION (Y,A2) is set
INTERSECTION ((UNION (Y,A1)),(UNION (Y,A2))) is set
a9 is set
f is set
f is set
f \/ f is set
g is set
g is set
g /\ g is set
f \/ g is set
f \/ g is set
(f \/ g) /\ (f \/ g) is set
X is set
K19(X) is non empty set
K19(K19(X)) is non empty set
X is set
K19(X) is non empty set
K19(K19(X)) is non empty set
{X} is non empty set
Y is Element of K19(K19(X))
A1 is set
A1 is set
A2 is set
X is non empty set
K19(X) is non empty set
K19(K19(X)) is non empty set
Y is Element of K19(X)
A1 is Element of K19(X)
(X,Y,A1) is (X)
{ b₁ where b₁ is Element of K19(X) : ( Y c= b₁ & b₁ c= A1 ) } is set
A2 is set
a9 is set
f is set
f is set
X is non empty set
K19(X) is non empty set
K19(K19(X)) is non empty set
Y is non empty (X)
(X,Y) is Element of K19(X)
(X,Y) is Element of K19(X)
(X,(X,Y),(X,Y)) is (X)
{ b₁ where b₁ is Element of K19(X) : ( (X,Y) c= b₁ & b₁ c= (X,Y) ) } is set
X is set
K19(X) is non empty set
K19(K19(X)) is non empty set
Y is non empty (X) Element of K19(K19(X))
meet Y is set
A1 is set
A2 is set
a9 is set
meet Y is Element of K19(X)
union Y is set
A1 is set
A2 is set
a9 is set
union Y is Element of K19(X)
X is set
K19(X) is non empty set
K19(K19(X)) is non empty set
Y is non empty (X) Element of K19(K19(X))
(X,Y) is Element of Y
A1 is set
A2 is set
X is set
K19(X) is non empty set
K19(K19(X)) is non empty set
Y is non empty (X) Element of K19(K19(X))
(X,Y) is Element of Y
A1 is set
A2 is set
X is non empty set
K19(X) is non empty set
K19(K19(X)) is non empty set
Y is Element of K19(X)
A1 is Element of K19(X)
(X,Y,A1) is (X)
{ b₁ where b₁ is Element of K19(X) : ( Y c= b₁ & b₁ c= A1 ) } is set
A2 is non empty (X) Element of K19(K19(X))
(X,A2) is Element of A2
(X,A2) is Element of A2
a9 is set
a9 is set
X is set
K19(X) is non empty set
K19(K19(X)) is non empty set
Y is set
A1 is non empty (X) Element of K19(K19(X))
(X,A1) is Element of A1
(X,A1) is Element of A1
A2 is set
a9 is set
X is non empty set
Y is non empty (X)
K19(X) is non empty set
K19(K19(X)) is non empty set
X is set
K19(X) is non empty set
K19(K19(X)) is non empty set
Y is non empty (X) Element of K19(K19(X))
A1 is non empty (X) Element of K19(K19(X))
A2 is non empty (X) Element of K19(K19(X))
INTERSECTION (A1,A2) is set
UNION (Y,(INTERSECTION (A1,A2))) is set
UNION (Y,A1) is set
UNION (Y,A2) is set
INTERSECTION ((UNION (Y,A1)),(UNION (Y,A2))) is set
a9 is set
f is set
f is set
f /\ f is set
g is set
g is set
g \/ g is set
a9 is set
a is set
a9 \/ a is set
g /\ (a9 \/ a) is set
g /\ (a9 \/ a) is set
(g /\ (a9 \/ a)) \/ (g /\ (a9 \/ a)) is set
g /\ a9 is set
g /\ a is set
(g /\ a9) \/ (g /\ a) is set
((g /\ a9) \/ (g /\ a)) \/ (g /\ (a9 \/ a)) is set
g /\ a9 is set
g /\ a is set
(g /\ a9) \/ (g /\ a) is set
((g /\ a9) \/ (g /\ a)) \/ ((g /\ a9) \/ (g /\ a)) is set
((g /\ a9) \/ (g /\ a)) \/ (g /\ a9) is set
(((g /\ a9) \/ (g /\ a)) \/ (g /\ a9)) \/ (g /\ a) is set
(X,Y) is Element of Y
(X,Y) is Element of Y
(X,Y) /\ (X,Y) is Element of K19(X)
(X,Y) /\ (X,Y) is Element of K19(X)
(g /\ a9) \/ (g /\ a9) is set
((g /\ a9) \/ (g /\ a9)) \/ (g /\ a) is set
X is set
K19(X) is non empty set
K19(K19(X)) is non empty set
Y is Element of K19(K19(X))
A1 is Element of K19(K19(X))
A2 is Element of K19(K19(X))
UNION (A1,A2) is set
INTERSECTION (Y,(UNION (A1,A2))) is set
INTERSECTION (Y,A1) is set
INTERSECTION (Y,A2) is set
UNION ((INTERSECTION (Y,A1)),(INTERSECTION (Y,A2))) is set
a9 is set
f is set
f is set
f /\ f is set
g is set
g is set
g \/ g is set
f /\ g is set
f /\ g is set
(f /\ g) \/ (f /\ g) is set
X is set
K19(X) is non empty set
K19(K19(X)) is non empty set
Y is non empty (X) Element of K19(K19(X))
A1 is non empty (X) Element of K19(K19(X))
A2 is non empty (X) Element of K19(K19(X))
UNION (A1,A2) is set
INTERSECTION (Y,(UNION (A1,A2))) is set
INTERSECTION (Y,A1) is set
INTERSECTION (Y,A2) is set
UNION ((INTERSECTION (Y,A1)),(INTERSECTION (Y,A2))) is set
a9 is set
f is set
f is set
f \/ f is set
g is set
g is set
g /\ g is set
a9 is set
a is set
a9 /\ a is set
(g /\ g) \/ a9 is set
(g /\ g) \/ a is set
((g /\ g) \/ a9) /\ ((g /\ g) \/ a) is set
a9 \/ (g /\ g) is set
a \/ g is set
a \/ g is set
(a \/ g) /\ (a \/ g) is set
(a9 \/ (g /\ g)) /\ ((a \/ g) /\ (a \/ g)) is set
a9 \/ g is set
a9 \/ g is set
(a9 \/ g) /\ (a9 \/ g) is set
((a9 \/ g) /\ (a9 \/ g)) /\ ((a \/ g) /\ (a \/ g)) is set
((a9 \/ g) /\ (a9 \/ g)) /\ (a \/ g) is set
(((a9 \/ g) /\ (a9 \/ g)) /\ (a \/ g)) /\ (a \/ g) is set
(X,Y) is Element of Y
(X,Y) is Element of Y
(X,Y) \/ (X,Y) is Element of K19(X)
(X,Y) /\ (X,Y) is Element of K19(X)
(a9 \/ g) /\ (a \/ g) is set
(a9 \/ g) /\ ((a9 \/ g) /\ (a \/ g)) is set
X is non empty set
Y is non empty (X)
A1 is non empty (X)
(X,Y,A1) is non empty (X)
UNION (Y,A1) is set
A2 is non empty (X)
(X,A1,A2) is non empty (X)
INTERSECTION (A1,A2) is set
(X,Y,(X,A1,A2)) is non empty (X)
UNION (Y,(X,A1,A2)) is set
(X,Y,A2) is non empty (X)
UNION (Y,A2) is set
(X,(X,Y,A1),(X,Y,A2)) is non empty (X)
INTERSECTION ((X,Y,A1),(X,Y,A2)) is set
a9 is set
f is set
f is set
f /\ f is set
K19(X) is non empty set
K19(K19(X)) is non empty set
INTERSECTION ((UNION (Y,A1)),(UNION (Y,A2))) is set
X is non empty set
Y is non empty (X)
A1 is non empty (X)
(X,Y,A1) is non empty (X)
INTERSECTION (Y,A1) is set
A2 is non empty (X)
(X,A1,A2) is non empty (X)
UNION (A1,A2) is set
(X,Y,(X,A1,A2)) is non empty (X)
INTERSECTION (Y,(X,A1,A2)) is set
(X,Y,A2) is non empty (X)
INTERSECTION (Y,A2) is set
(X,(X,Y,A1),(X,Y,A2)) is non empty (X)
UNION ((X,Y,A1),(X,Y,A2)) is set
a9 is set
f is set
f is set
f /\ f is set
g is set
g is set
g \/ g is set
K19(X) is non empty set
K19(K19(X)) is non empty set
f /\ (g \/ g) is set
INTERSECTION (Y,(UNION (A1,A2))) is set
a9 is set
f is set
f is set
f \/ f is set
K19(X) is non empty set
K19(K19(X)) is non empty set
UNION ((INTERSECTION (Y,A1)),(INTERSECTION (Y,A2))) is set
X is set
K19(X) is non empty set
K19(K19(X)) is non empty set
Y is non empty (X) Element of K19(K19(X))
A1 is non empty (X) Element of K19(K19(X))
UNION (Y,A1) is set
INTERSECTION (Y,(UNION (Y,A1))) is set
(X,Y) is Element of Y
(X,Y) is Element of Y
f is set
f is set
g is set
f /\ g is set
g is set
a9 is set
g \/ a9 is set
f /\ g is set
f /\ a9 is set
(f /\ g) \/ (f /\ a9) is set
(X,Y) /\ (X,Y) is Element of K19(X)
f is set
the Element of A1 is Element of A1
f \/ the Element of A1 is set
f /\ (f \/ the Element of A1) is set
X is set
K19(X) is non empty set
K19(K19(X)) is non empty set
Y is non empty (X) Element of K19(K19(X))
A1 is non empty (X) Element of K19(K19(X))
INTERSECTION (Y,A1) is set
UNION ((INTERSECTION (Y,A1)),A1) is set
A2 is set
(X,A1) is Element of A1
(X,A1) is Element of A1
f is set
g is set
f \/ g is set
g is set
a9 is set
g /\ a9 is set
A2 is set
the Element of Y is Element of Y
A2 /\ the Element of Y is Element of K19(X)
A2 \/ (A2 /\ the Element of Y) is set
the Element of Y /\ A2 is Element of K19(X)
X is non empty set
Y is non empty (X)
A1 is non empty (X)
(X,Y,A1) is non empty (X)
UNION (Y,A1) is set
(X,Y,(X,Y,A1)) is non empty (X)
INTERSECTION (Y,(X,Y,A1)) is set
K19(X) is non empty set
K19(K19(X)) is non empty set
X is non empty set
Y is non empty (X)
A1 is non empty (X)
(X,Y,A1) is non empty (X)
INTERSECTION (Y,A1) is set
(X,(X,Y,A1),A1) is non empty (X)
UNION ((X,Y,A1),A1) is set
K19(X) is non empty set
K19(K19(X)) is non empty set
X is non empty set
K19(X) is non empty set
K19(K19(X)) is non empty set
Y is Element of K19(K19(X))
A1 is Element of K19(K19(X))
DIFFERENCE (Y,A1) is set
bool X is non empty Element of K19(K19(X))
A2 is set
a9 is set
f is set
a9 \ f is Element of K19(a9)
K19(a9) is non empty set
X is non empty set
K19(X) is non empty set
K19(K19(X)) is non empty set
Y is non empty (X) Element of K19(K19(X))
A1 is non empty (X) Element of K19(K19(X))
DIFFERENCE (Y,A1) is set
(X,Y) is Element of Y
(X,A1) is Element of A1
(X,Y) \ (X,A1) is Element of K19(X)
(X,Y) is Element of Y
(X,A1) is Element of A1
(X,Y) \ (X,A1) is Element of K19(X)
{ b₁ where b₁ is Element of K19(X) : ( (X,Y) \ (X,A1) c= b₁ & b₁ c= (X,Y) \ (X,A1) ) } is set
g is set
g is set
a9 is set
g \ a9 is Element of K19(g)
K19(g) is non empty set
a is Element of K19(X)
g is set
g is Element of K19(X)
g \/ (X,Y) is Element of K19(X)
(g \/ (X,Y)) /\ (X,Y) is Element of K19(X)
(X,A1) ` is Element of K19(X)
X \ (X,A1) is set
g \/ ((X,A1) `) is Element of K19(X)
(X,A1) ` is Element of K19(X)
X \ (X,A1) is set
(g \/ ((X,A1) `)) /\ ((X,A1) `) is Element of K19(X)
((g \/ ((X,A1) `)) /\ ((X,A1) `)) ` is Element of K19(X)
X \ ((g \/ ((X,A1) `)) /\ ((X,A1) `)) is set
g /\ ((X,A1) `) is Element of K19(X)
((X,A1) `) /\ ((X,A1) `) is Element of K19(X)
(g /\ ((X,A1) `)) \/ (((X,A1) `) /\ ((X,A1) `)) is Element of K19(X)
(g /\ ((X,A1) `)) \/ ((X,A1) `) is Element of K19(X)
((X,A1) `) ` is Element of K19(X)
X \ ((X,A1) `) is set
((X,A1) `) ` is Element of K19(X)
X \ ((X,A1) `) is set
g /\ (X,Y) is Element of K19(X)
(X,Y) /\ (X,Y) is Element of K19(X)
(g /\ (X,Y)) \/ ((X,Y) /\ (X,Y)) is Element of K19(X)
(g /\ (X,Y)) \/ (X,Y) is Element of K19(X)
g \/ ((X,Y) \ (X,A1)) is Element of K19(X)
(g \/ ((X,Y) \ (X,A1))) /\ ((X,Y) \ (X,A1)) is Element of K19(X)
g /\ ((X,Y) \ (X,A1)) is Element of K19(X)
((g \/ (X,Y)) /\ (X,Y)) \ (((g \/ ((X,A1) `)) /\ ((X,A1) `)) `) is Element of K19(X)
(((g \/ ((X,A1) `)) /\ ((X,A1) `)) `) ` is Element of K19(X)
X \ (((g \/ ((X,A1) `)) /\ ((X,A1) `)) `) is set
((g \/ (X,Y)) /\ (X,Y)) /\ ((((g \/ ((X,A1) `)) /\ ((X,A1) `)) `) `) is Element of K19(X)
(X,Y) /\ ((g \/ ((X,A1) `)) /\ ((X,A1) `)) is Element of K19(X)
(g \/ (X,Y)) /\ ((X,Y) /\ ((g \/ ((X,A1) `)) /\ ((X,A1) `))) is Element of K19(X)
((X,A1) `) /\ (X,Y) is Element of K19(X)
(g \/ ((X,A1) `)) /\ (((X,A1) `) /\ (X,Y)) is Element of K19(X)
(g \/ (X,Y)) /\ ((g \/ ((X,A1) `)) /\ (((X,A1) `) /\ (X,Y))) is Element of K19(X)
(g \/ ((X,A1) `)) /\ ((X,Y) \ (X,A1)) is Element of K19(X)
(g \/ (X,Y)) /\ ((g \/ ((X,A1) `)) /\ ((X,Y) \ (X,A1))) is Element of K19(X)
(g \/ (X,Y)) /\ (g \/ ((X,A1) `)) is Element of K19(X)
((g \/ (X,Y)) /\ (g \/ ((X,A1) `))) /\ ((X,Y) \ (X,A1)) is Element of K19(X)
(X,Y) /\ ((X,A1) `) is Element of K19(X)
g \/ ((X,Y) /\ ((X,A1) `)) is Element of K19(X)
(g \/ ((X,Y) /\ ((X,A1) `))) /\ ((X,Y) \ (X,A1)) is Element of K19(X)
X is non empty set
K19(X) is non empty set
Y is Element of K19(X)
A1 is Element of K19(X)
A2 is Element of K19(X)
a9 is Element of K19(X)
(X,Y,A1) is (X)
{ b₁ where b₁ is Element of K19(X) : ( Y c= b₁ & b₁ c= A1 ) } is set
(X,A2,a9) is (X)
{ b₁ where b₁ is Element of K19(X) : ( A2 c= b₁ & b₁ c= a9 ) } is set
DIFFERENCE ((X,Y,A1),(X,A2,a9)) is set
Y \ a9 is Element of K19(X)
A1 \ A2 is Element of K19(X)
{ b₁ where b₁ is Element of K19(X) : ( Y \ a9 c= b₁ & b₁ c= A1 \ A2 ) } is set
K19(K19(X)) is non empty set
f is non empty (X) Element of K19(K19(X))
(X,f) is Element of f
(X,f) is Element of f
f is non empty (X) Element of K19(K19(X))
(X,f) is Element of f
(X,f) is Element of f
X is non empty set
Y is non empty (X)
A1 is non empty (X)
DIFFERENCE (Y,A1) is set
K19(X) is non empty set
a9 is Element of K19(X)
f is Element of K19(X)
(X,a9,f) is (X)
{ b₁ where b₁ is Element of K19(X) : ( a9 c= b₁ & b₁ c= f ) } is set
f is Element of K19(X)
g is Element of K19(X)
(X,f,g) is (X)
{ b₁ where b₁ is Element of K19(X) : ( f c= b₁ & b₁ c= g ) } is set
a9 \ g is Element of K19(X)
f \ f is Element of K19(X)
(X,(a9 \ g),(f \ f)) is (X)
{ b₁ where b₁ is Element of K19(X) : ( a9 \ g c= b₁ & b₁ c= f \ f ) } is set
X is non empty set
Y is non empty (X)
A1 is non empty (X)
(X,Y,A1) is (X)
DIFFERENCE (Y,A1) is set
K19(X) is non empty set
A2 is Element of K19(X)
a9 is Element of K19(X)
(X,A2,a9) is (X)
{ b₁ where b₁ is Element of K19(X) : ( A2 c= b₁ & b₁ c= a9 ) } is set
f is Element of K19(X)
f is Element of K19(X)
(X,f,f) is (X)
{ b₁ where b₁ is Element of K19(X) : ( f c= b₁ & b₁ c= f ) } is set
A2 \ f is Element of K19(X)
g is set
X is non empty set
Y is non empty (X)
(X,Y) is Element of K19(X)
K19(X) is non empty set
(X,Y) is Element of K19(X)
A1 is non empty (X)
(X,Y,A1) is non empty (X)
DIFFERENCE (Y,A1) is set
(X,A1) is Element of K19(X)
(X,Y) \ (X,A1) is Element of K19(X)
(X,A1) is Element of K19(X)
(X,Y) \ (X,A1) is Element of K19(X)
(X,((X,Y) \ (X,A1)),((X,Y) \ (X,A1))) is (X)
{ b₁ where b₁ is Element of K19(X) : ( (X,Y) \ (X,A1) c= b₁ & b₁ c= (X,Y) \ (X,A1) ) } is set
K19(K19(X)) is non empty set
A2 is non empty (X) Element of K19(K19(X))
(X,(X,Y),(X,Y)) is (X)
{ b₁ where b₁ is Element of K19(X) : ( (X,Y) c= b₁ & b₁ c= (X,Y) ) } is set
a9 is non empty (X) Element of K19(K19(X))
(X,(X,A1),(X,A1)) is (X)
{ b₁ where b₁ is Element of K19(X) : ( (X,A1) c= b₁ & b₁ c= (X,A1) ) } is set
(X,A2) is Element of A2
(X,a9) is Element of a9
(X,A2) is Element of A2
(X,a9) is Element of a9
X is non empty set
K19(X) is non empty set
Y is non empty (X)
A1 is non empty (X)
(X,Y,A1) is non empty (X)
DIFFERENCE (Y,A1) is set
(X,A1) is Element of K19(X)
(X,A1) is Element of K19(X)
A2 is Element of K19(X)
a9 is Element of K19(X)
(X,A2,a9) is (X)
{ b₁ where b₁ is Element of K19(X) : ( A2 c= b₁ & b₁ c= a9 ) } is set
A2 \ (X,A1) is Element of K19(X)
a9 \ (X,A1) is Element of K19(X)
(X,(A2 \ (X,A1)),(a9 \ (X,A1))) is (X)
{ b₁ where b₁ is Element of K19(X) : ( A2 \ (X,A1) c= b₁ & b₁ c= a9 \ (X,A1) ) } is set
(X,Y) is Element of K19(X)
(X,Y) is Element of K19(X)
(X,(X,Y),(X,Y)) is (X)
{ b₁ where b₁ is Element of K19(X) : ( (X,Y) c= b₁ & b₁ c= (X,Y) ) } is set
X is non empty set
K19(X) is non empty set
Y is non empty (X)
A1 is non empty (X)
(X,Y,A1) is non empty (X)
DIFFERENCE (Y,A1) is set
A2 is Element of K19(X)
a9 is Element of K19(X)
(X,A2,a9) is (X)
{ b₁ where b₁ is Element of K19(X) : ( A2 c= b₁ & b₁ c= a9 ) } is set
f is Element of K19(X)
f is Element of K19(X)
(X,f,f) is (X)
{ b₁ where b₁ is Element of K19(X) : ( f c= b₁ & b₁ c= f ) } is set
A2 \ f is Element of K19(X)
a9 \ f is Element of K19(X)
(X,(A2 \ f),(a9 \ f)) is (X)
{ b₁ where b₁ is Element of K19(X) : ( A2 \ f c= b₁ & b₁ c= a9 \ f ) } is set
(X,Y) is Element of K19(X)
(X,Y) is Element of K19(X)
(X,(X,Y),(X,Y)) is (X)
{ b₁ where b₁ is Element of K19(X) : ( (X,Y) c= b₁ & b₁ c= (X,Y) ) } is set
(X,A1) is Element of K19(X)
(X,A1) is Element of K19(X)
(X,(X,A1),(X,A1)) is (X)
{ b₁ where b₁ is Element of K19(X) : ( (X,A1) c= b₁ & b₁ c= (X,A1) ) } is set
X is non empty set
[#] X is non empty non proper Element of K19(X)
K19(X) is non empty set
(X,([#] X),([#] X)) is (X)
{ b₁ where b₁ is Element of K19(X) : ( [#] X c= b₁ & b₁ c= [#] X ) } is set
{([#] X)} is non empty set
X is non empty set
{} X is empty proper Element of K19(X)
K19(X) is non empty set
(X,({} X),({} X)) is (X)
{ b₁ where b₁ is Element of K19(X) : ( {} X c= b₁ & b₁ c= {} X ) } is set
{{}} is non empty set
X is non empty set
[#] X is non empty non proper Element of K19(X)
K19(X) is non empty set
(X,([#] X),([#] X)) is (X)
{ b₁ where b₁ is Element of K19(X) : ( [#] X c= b₁ & b₁ c= [#] X ) } is set
{} X is empty proper Element of K19(X)
(X,({} X),({} X)) is (X)
{ b₁ where b₁ is Element of K19(X) : ( {} X c= b₁ & b₁ c= {} X ) } is set
X is non empty set
[#] X is non empty non proper Element of K19(X)
K19(X) is non empty set
(X,([#] X),([#] X)) is non empty (X)
{ b₁ where b₁ is Element of K19(X) : ( [#] X c= b₁ & b₁ c= [#] X ) } is set
Y is non empty (X)
(X,(X,([#] X),([#] X)),Y) is non empty (X)
DIFFERENCE ((X,([#] X),([#] X)),Y) is set
X is non empty set
Y is non empty (X)
(X,Y) is non empty (X)
[#] X is non empty non proper Element of K19(X)
K19(X) is non empty set
(X,([#] X),([#] X)) is non empty (X)
{ b₁ where b₁ is Element of K19(X) : ( [#] X c= b₁ & b₁ c= [#] X ) } is set
(X,(X,([#] X),([#] X)),Y) is non empty (X)
DIFFERENCE ((X,([#] X),([#] X)),Y) is set
(X,Y) is Element of K19(X)
(X,Y) ` is Element of K19(X)
X \ (X,Y) is set
(X,Y) is Element of K19(X)
(X,Y) ` is Element of K19(X)
X \ (X,Y) is set
(X,((X,Y) `),((X,Y) `)) is (X)
{ b₁ where b₁ is Element of K19(X) : ( (X,Y) ` c= b<sub>1</sub> & b<sub>1</sub> c= (X,Y) ` ) } is set
X is non empty set
K19(X) is non empty set
Y is non empty (X)
(X,Y) is non empty (X)
[#] X is non empty non proper Element of K19(X)
(X,([#] X),([#] X)) is non empty (X)
{ b₁ where b₁ is Element of K19(X) : ( [#] X c= b₁ & b₁ c= [#] X ) } is set
(X,(X,([#] X),([#] X)),Y) is non empty (X)
DIFFERENCE ((X,([#] X),([#] X)),Y) is set
A1 is Element of K19(X)
A2 is Element of K19(X)
(X,A1,A2) is (X)
{ b₁ where b₁ is Element of K19(X) : ( A1 c= b₁ & b₁ c= A2 ) } is set
A2 ` is Element of K19(X)
X \ A2 is set
A1 ` is Element of K19(X)
X \ A1 is set
(X,(A2 `),(A1 `)) is (X)
{ b₁ where b₁ is Element of K19(X) : ( A2 ` c= b<sub>1</sub> & b<sub>1</sub> c= A1 ` ) } is set
(X,Y) is Element of K19(X)
(X,Y) is Element of K19(X)
(X,(X,Y),(X,Y)) is (X)
{ b₁ where b₁ is Element of K19(X) : ( (X,Y) c= b₁ & b₁ c= (X,Y) ) } is set
X is non empty set
{} X is empty proper Element of K19(X)
K19(X) is non empty set
(X,({} X),({} X)) is non empty (X)
{ b₁ where b₁ is Element of K19(X) : ( {} X c= b₁ & b₁ c= {} X ) } is set
(X,(X,({} X),({} X))) is non empty (X)
[#] X is non empty non proper Element of K19(X)
(X,([#] X),([#] X)) is non empty (X)
{ b₁ where b₁ is Element of K19(X) : ( [#] X c= b₁ & b₁ c= [#] X ) } is set
(X,(X,([#] X),([#] X)),(X,({} X),({} X))) is non empty (X)
DIFFERENCE ((X,([#] X),([#] X)),(X,({} X),({} X))) is set
({} X) ` is Element of K19(X)
X \ ({} X) is set
(X,([#] X),(({} X) `)) is (X)
{ b₁ where b₁ is Element of K19(X) : ( [#] X c= b₁ & b₁ c= ({} X) ` ) } is set
X is non empty set
[#] X is non empty non proper Element of K19(X)
K19(X) is non empty set
(X,([#] X),([#] X)) is non empty (X)
{ b<sub>1</sub> where b<sub>1</sub> is Element of K19(X) : ( [#] X c= b<sub>1</sub> & b<sub>1</sub> c= [#] X ) } is set
(X,(X,([#] X),([#] X))) is non empty (X)
(X,(X,([#] X),([#] X)),(X,([#] X),([#] X))) is non empty (X)
DIFFERENCE ((X,([#] X),([#] X)),(X,([#] X),([#] X))) is set
{} X is empty proper Element of K19(X)
(X,({} X),({} X)) is non empty (X)
{ b<sub>1</sub> where b<sub>1</sub> is Element of K19(X) : ( {} X c= b<sub>1</sub> & b<sub>1</sub> c= {} X ) } is set
([#] X) ` is Element of K19(X)
X \ ([#] X) is set
(X,(([#] X) `),(([#] X) `)) is (X)
{ b₁ where b₁ is Element of K19(X) : ( ([#] X) ` c= b<sub>1</sub> & b<sub>1</sub> c= ([#] X) ` ) } is set
(X,({} X),(([#] X) `)) is (X)
{ b<sub>1</sub> where b<sub>1</sub> is Element of K19(X) : ( {} X c= b<sub>1</sub> & b<sub>1</sub> c= ([#] X) ` ) } is set
X is non empty set
{} X is empty proper Element of K19(X)
K19(X) is non empty set
(X,({} X),({} X)) is non empty (X)
{ b₁ where b₁ is Element of K19(X) : ( {} X c= b₁ & b₁ c= {} X ) } is set
[#] X is non empty non proper Element of K19(X)
(X,({} X),([#] X)) is (X)
{ b₁ where b₁ is Element of K19(X) : ( {} X c= b₁ & b₁ c= [#] X ) } is set
Y is non empty (X)
(X,Y) is non empty (X)
(X,([#] X),([#] X)) is non empty (X)
{ b₁ where b₁ is Element of K19(X) : ( [#] X c= b₁ & b₁ c= [#] X ) } is set
(X,(X,([#] X),([#] X)),Y) is non empty (X)
DIFFERENCE ((X,([#] X),([#] X)),Y) is set
([#] X) ` is Element of K19(X)
X \ ([#] X) is set
({} X) ` is Element of K19(X)
X \ ({} X) is set
(X,(([#] X) `),(({} X) `)) is (X)
{ b₁ where b₁ is Element of K19(X) : ( ([#] X) ` c= b<sub>1</sub> & b<sub>1</sub> c= ({} X) ` ) } is set
(X,(X,Y)) is Element of K19(X)
(X,(X,Y)) is Element of K19(X)
(X,(X,(X,Y)),(X,(X,Y))) is (X)
{ b₁ where b₁ is Element of K19(X) : ( (X,(X,Y)) c= b₁ & b₁ c= (X,(X,Y)) ) } is set
(X,Y,Y) is non empty (X)
INTERSECTION (Y,Y) is set
(X,(X,Y,Y)) is non empty (X)
(X,(X,([#] X),([#] X)),(X,Y,Y)) is non empty (X)
DIFFERENCE ((X,([#] X),([#] X)),(X,Y,Y)) is set
({} X) /\ ({} X) is Element of K19(X)
([#] X) /\ ([#] X) is Element of K19(X)
(X,(({} X) /\ ({} X)),(([#] X) /\ ([#] X))) is (X)
{ b₁ where b₁ is Element of K19(X) : ( ({} X) /\ ({} X) c= b₁ & b₁ c= ([#] X) /\ ([#] X) ) } is set
X is non empty set
[#] X is non empty non proper Element of K19(X)
K19(X) is non empty set
(X,([#] X),([#] X)) is non empty (X)
{ b₁ where b₁ is Element of K19(X) : ( [#] X c= b₁ & b₁ c= [#] X ) } is set
{} X is empty proper Element of K19(X)
(X,({} X),([#] X)) is (X)
{ b₁ where b₁ is Element of K19(X) : ( {} X c= b₁ & b₁ c= [#] X ) } is set
Y is non empty (X)
(X,Y) is non empty (X)
(X,(X,([#] X),([#] X)),Y) is non empty (X)
DIFFERENCE ((X,([#] X),([#] X)),Y) is set
([#] X) ` is Element of K19(X)
X \ ([#] X) is set
({} X) ` is Element of K19(X)
X \ ({} X) is set
(X,(([#] X) `),(({} X) `)) is (X)
{ b₁ where b₁ is Element of K19(X) : ( ([#] X) ` c= b<sub>1</sub> & b<sub>1</sub> c= ({} X) ` ) } is set
(X,(X,Y)) is Element of K19(X)
(X,(X,Y)) is Element of K19(X)
(X,(X,(X,Y)),(X,(X,Y))) is (X)
{ b₁ where b₁ is Element of K19(X) : ( (X,(X,Y)) c= b₁ & b₁ c= (X,(X,Y)) ) } is set
(X,Y,Y) is non empty (X)
UNION (Y,Y) is set
(X,(X,Y,Y)) is non empty (X)
(X,(X,([#] X),([#] X)),(X,Y,Y)) is non empty (X)
DIFFERENCE ((X,([#] X),([#] X)),(X,Y,Y)) is set
({} X) \/ ({} X) is Element of K19(X)
([#] X) \/ ([#] X) is non empty Element of K19(X)
(X,(({} X) \/ ({} X)),(([#] X) \/ ([#] X))) is (X)
{ b₁ where b₁ is Element of K19(X) : ( ({} X) \/ ({} X) c= b₁ & b₁ c= ([#] X) \/ ([#] X) ) } is set
X is non empty set
{} X is empty proper Element of K19(X)
K19(X) is non empty set
(X,({} X),({} X)) is non empty (X)
{ b₁ where b₁ is Element of K19(X) : ( {} X c= b₁ & b₁ c= {} X ) } is set
[#] X is non empty non proper Element of K19(X)
(X,({} X),([#] X)) is (X)
{ b₁ where b₁ is Element of K19(X) : ( {} X c= b₁ & b₁ c= [#] X ) } is set
Y is non empty (X)
(X,Y,Y) is non empty (X)
DIFFERENCE (Y,Y) is set
({} X) \ ([#] X) is Element of K19(X)
([#] X) \ ({} X) is Element of K19(X)
(X,(({} X) \ ([#] X)),(([#] X) \ ({} X))) is (X)
{ b₁ where b₁ is Element of K19(X) : ( ({} X) \ ([#] X) c= b₁ & b₁ c= ([#] X) \ ({} X) ) } is set
X is non empty set
Y is non empty (X)
(X,Y) is non empty (X)
[#] X is non empty non proper Element of K19(X)
K19(X) is non empty set
(X,([#] X),([#] X)) is non empty (X)
{ b₁ where b₁ is Element of K19(X) : ( [#] X c= b₁ & b₁ c= [#] X ) } is set
(X,(X,([#] X),([#] X)),Y) is non empty (X)
DIFFERENCE ((X,([#] X),([#] X)),Y) is set
(X,Y,(X,Y)) is non empty (X)
UNION (Y,(X,Y)) is set
(X,Y) is Element of K19(X)
(X,Y) is Element of K19(X)
(X,Y) ` is Element of K19(X)
X \ (X,Y) is set
(X,Y) \/ ((X,Y) `) is Element of K19(X)
A1 is set
(X,Y) ` is Element of K19(X)
X \ (X,Y) is set
(X,Y) ` is Element of K19(X)
X \ (X,Y) is set
(X,((X,Y) `),((X,Y) `)) is (X)
{ b₁ where b₁ is Element of K19(X) : ( (X,Y) ` c= b<sub>1</sub> & b<sub>1</sub> c= (X,Y) ` ) } is set
(X,(X,Y)) is Element of K19(X)
(X,(X,Y)) is Element of K19(X)
(X,(X,(X,Y)),(X,(X,Y))) is (X)
{ b₁ where b₁ is Element of K19(X) : ( (X,(X,Y)) c= b₁ & b₁ c= (X,(X,Y)) ) } is set
(X,Y) \/ ((X,Y) `) is Element of K19(X)
(X,((X,Y) \/ ((X,Y) `)),((X,Y) \/ ((X,Y) `))) is (X)
{ b<sub>1</sub> where b<sub>1</sub> is Element of K19(X) : ( (X,Y) \/ ((X,Y) `) c= b₁ & b₁ c= (X,Y) \/ ((X,Y) `) ) } is set
X is non empty set
Y is non empty (X)
(X,Y) is non empty (X)
[#] X is non empty non proper Element of K19(X)
K19(X) is non empty set
(X,([#] X),([#] X)) is non empty (X)
{ b<sub>1</sub> where b<sub>1</sub> is Element of K19(X) : ( [#] X c= b<sub>1</sub> & b<sub>1</sub> c= [#] X ) } is set
(X,(X,([#] X),([#] X)),Y) is non empty (X)
DIFFERENCE ((X,([#] X),([#] X)),Y) is set
(X,Y,(X,Y)) is non empty (X)
INTERSECTION (Y,(X,Y)) is set
(X,Y) is Element of K19(X)
(X,Y) is Element of K19(X)
(X,Y) ` is Element of K19(X)
X \ (X,Y) is set
(X,Y) /\ ((X,Y) `) is Element of K19(X)
A1 is set
(X,Y) ` is Element of K19(X)
X \ (X,Y) is set
(X,((X,Y) `),((X,Y) `)) is (X)
{ b₁ where b₁ is Element of K19(X) : ( (X,Y) ` c= b<sub>1</sub> & b<sub>1</sub> c= (X,Y) ` ) } is set
(X,(X,Y)) is Element of K19(X)
(X,(X,Y)) is Element of K19(X)
(X,(X,(X,Y)),(X,(X,Y))) is (X)
{ b₁ where b₁ is Element of K19(X) : ( (X,(X,Y)) c= b₁ & b₁ c= (X,(X,Y)) ) } is set
(X,Y) /\ ((X,Y) `) is Element of K19(X)
(X,((X,Y) /\ ((X,Y) `)),((X,Y) /\ ((X,Y) `))) is (X)
{ b<sub>1</sub> where b<sub>1</sub> is Element of K19(X) : ( (X,Y) /\ ((X,Y) `) c= b₁ & b₁ c= (X,Y) /\ ((X,Y) `) ) } is set
X is non empty set
Y is non empty (X)
(X,Y,Y) is non empty (X)
DIFFERENCE (Y,Y) is set
(X,Y) is Element of K19(X)
K19(X) is non empty set
(X,Y) is Element of K19(X)
(X,Y) \ (X,Y) is Element of K19(X)
(X,Y) \ (X,Y) is Element of K19(X)
(X,((X,Y) \ (X,Y)),((X,Y) \ (X,Y))) is (X)
{ b<sub>1</sub> where b<sub>1</sub> is Element of K19(X) : ( (X,Y) \ (X,Y) c= b<sub>1</sub> & b<sub>1</sub> c= (X,Y) \ (X,Y) ) } is set
A1 is set
X is non empty set
bool X is non empty Element of K19(K19(X))
K19(X) is non empty set
K19(K19(X)) is non empty set
bool (bool X) is non empty Element of K19(K19((bool X)))
K19((bool X)) is non empty set
K19(K19((bool X))) is non empty set
Y is set
Y is set
the Element of X is Element of X
{ the Element of X} is non empty set
A2 is Element of K19(X)
{A2} is non empty set
a9 is non empty set
f is set
f is set
Y is non empty set
A1 is non empty set
A2 is set
X is non empty set
(X) is non empty set
A1 is Element of (X)
A2 is Element of (X)
a9 is non empty (X)
f is non empty (X)
(X,a9,f) is non empty (X)
UNION (a9,f) is set
f is Element of (X)
K20((X),(X)) is non empty set
K20(K20((X),(X)),(X)) is non empty set
K19(K20(K20((X),(X)),(X))) is non empty set
A1 is V1() V4(K20((X),(X))) V5((X)) V6() V18(K20((X),(X)),(X)) Element of K19(K20(K20((X),(X)),(X)))
A2 is Element of (X)
a9 is Element of (X)
f is non empty (X)
f is non empty (X)
(X,f,f) is non empty (X)
INTERSECTION (f,f) is set
g is Element of (X)
A2 is V1() V4(K20((X),(X))) V5((X)) V6() V18(K20((X),(X)),(X)) Element of K19(K20(K20((X),(X)),(X)))
LattStr(# (X),A1,A2 #) is non empty strict LattStr
a9 is non empty strict LattStr
the carrier of a9 is non empty set
the L_join of a9 is V1() V4(K20( the carrier of a9, the carrier of a9)) V5( the carrier of a9) V6() V18(K20( the carrier of a9, the carrier of a9), the carrier of a9) Element of K19(K20(K20( the carrier of a9, the carrier of a9), the carrier of a9))
K20( the carrier of a9, the carrier of a9) is non empty set
K20(K20( the carrier of a9, the carrier of a9), the carrier of a9) is non empty set
K19(K20(K20( the carrier of a9, the carrier of a9), the carrier of a9)) is non empty set
the L_meet of a9 is V1() V4(K20( the carrier of a9, the carrier of a9)) V5( the carrier of a9) V6() V18(K20( the carrier of a9, the carrier of a9), the carrier of a9) Element of K19(K20(K20( the carrier of a9, the carrier of a9), the carrier of a9))
f is Element of the carrier of a9
f is Element of the carrier of a9
the L_join of a9 . (f,f) is Element of the carrier of a9
the L_meet of a9 . (f,f) is Element of the carrier of a9
g is non empty (X)
g is non empty (X)
(X,g,g) is non empty (X)
UNION (g,g) is set
(X,g,g) is non empty (X)
INTERSECTION (g,g) is set
a9 is Element of (X)
a is Element of (X)
A1 . (a9,a) is Element of (X)
b is non empty (X)
b9 is non empty (X)
(X,b,b9) is non empty (X)
UNION (b,b9) is set
A2 . (a9,a) is Element of (X)
a9 is non empty (X)
Z1 is non empty (X)
(X,a9,Z1) is non empty (X)
INTERSECTION (a9,Z1) is set
Y is non empty strict LattStr
the carrier of Y is non empty set
the L_join of Y is V1() V4(K20( the carrier of Y, the carrier of Y)) V5( the carrier of Y) V6() V18(K20( the carrier of Y, the carrier of Y), the carrier of Y) Element of K19(K20(K20( the carrier of Y, the carrier of Y), the carrier of Y))
K20( the carrier of Y, the carrier of Y) is non empty set
K20(K20( the carrier of Y, the carrier of Y), the carrier of Y) is non empty set
K19(K20(K20( the carrier of Y, the carrier of Y), the carrier of Y)) is non empty set
the L_meet of Y is V1() V4(K20( the carrier of Y, the carrier of Y)) V5( the carrier of Y) V6() V18(K20( the carrier of Y, the carrier of Y), the carrier of Y) Element of K19(K20(K20( the carrier of Y, the carrier of Y), the carrier of Y))
A1 is non empty strict LattStr
the carrier of A1 is non empty set
the L_join of A1 is V1() V4(K20( the carrier of A1, the carrier of A1)) V5( the carrier of A1) V6() V18(K20( the carrier of A1, the carrier of A1), the carrier of A1) Element of K19(K20(K20( the carrier of A1, the carrier of A1), the carrier of A1))
K20( the carrier of A1, the carrier of A1) is non empty set
K20(K20( the carrier of A1, the carrier of A1), the carrier of A1) is non empty set
K19(K20(K20( the carrier of A1, the carrier of A1), the carrier of A1)) is non empty set
the L_meet of A1 is V1() V4(K20( the carrier of A1, the carrier of A1)) V5( the carrier of A1) V6() V18(K20( the carrier of A1, the carrier of A1), the carrier of A1) Element of K19(K20(K20( the carrier of A1, the carrier of A1), the carrier of A1))
A2 is Element of the carrier of Y
a9 is Element of the carrier of Y
the L_join of Y . (A2,a9) is Element of the carrier of Y
the L_join of A1 . (A2,a9) is set
f is non empty (X)
f is non empty (X)
(X,f,f) is non empty (X)
UNION (f,f) is set
A2 is Element of the carrier of Y
a9 is Element of the carrier of Y
the L_meet of Y . (A2,a9) is Element of the carrier of Y
the L_meet of A1 . (A2,a9) is set
f is non empty (X)
f is non empty (X)
(X,f,f) is non empty (X)
INTERSECTION (f,f) is set
X is non empty set
(X) is non empty strict LattStr
the carrier of (X) is non empty set
Y is Element of the carrier of (X)
A1 is Element of the carrier of (X)
Y "\/" A1 is Element of the carrier of (X)
the L_join of (X) is V1() V4(K20( the carrier of (X), the carrier of (X))) V5( the carrier of (X)) V6() V18(K20( the carrier of (X), the carrier of (X)), the carrier of (X)) Element of K19(K20(K20( the carrier of (X), the carrier of (X)), the carrier of (X)))
K20( the carrier of (X), the carrier of (X)) is non empty set
K20(K20( the carrier of (X), the carrier of (X)), the carrier of (X)) is non empty set
K19(K20(K20( the carrier of (X), the carrier of (X)), the carrier of (X))) is non empty set
the L_join of (X) . (Y,A1) is Element of the carrier of (X)
A1 "\/" Y is Element of the carrier of (X)
the L_join of (X) . (A1,Y) is Element of the carrier of (X)
(X) is non empty set
A2 is non empty (X)
a9 is non empty (X)
(X,A2,a9) is non empty (X)
UNION (A2,a9) is set
(X,a9,A2) is non empty (X)
UNION (a9,A2) is set
the carrier of (X) is non empty set
Y is Element of the carrier of (X)
A1 is Element of the carrier of (X)
A2 is Element of the carrier of (X)
A1 "\/" A2 is Element of the carrier of (X)
the L_join of (X) is V1() V4(K20( the carrier of (X), the carrier of (X))) V5( the carrier of (X)) V6() V18(K20( the carrier of (X), the carrier of (X)), the carrier of (X)) Element of K19(K20(K20( the carrier of (X), the carrier of (X)), the carrier of (X)))
K20( the carrier of (X), the carrier of (X)) is non empty set
K20(K20( the carrier of (X), the carrier of (X)), the carrier of (X)) is non empty set
K19(K20(K20( the carrier of (X), the carrier of (X)), the carrier of (X))) is non empty set
the L_join of (X) . (A1,A2) is Element of the carrier of (X)
Y "\/" (A1 "\/" A2) is Element of the carrier of (X)
the L_join of (X) . (Y,(A1 "\/" A2)) is Element of the carrier of (X)
Y "\/" A1 is Element of the carrier of (X)
the L_join of (X) . (Y,A1) is Element of the carrier of (X)
(Y "\/" A1) "\/" A2 is Element of the carrier of (X)
the L_join of (X) . ((Y "\/" A1),A2) is Element of the carrier of (X)
(X) is non empty set
f is non empty (X)
f is non empty (X)
(X,f,f) is non empty (X)
UNION (f,f) is set
a9 is non empty (X)
(X,a9,f) is non empty (X)
UNION (a9,f) is set
g is non empty (X)
g is non empty (X)
the L_join of (X) . (Y,g) is set
(X,a9,g) is non empty (X)
UNION (a9,g) is set
(X,(X,a9,f),f) is non empty (X)
UNION ((X,a9,f),f) is set
the L_join of (X) . (g,f) is set
the carrier of (X) is non empty set
Y is Element of the carrier of (X)
A1 is Element of the carrier of (X)
Y "/\" A1 is Element of the carrier of (X)
the L_meet of (X) is V1() V4(K20( the carrier of (X), the carrier of (X))) V5( the carrier of (X)) V6() V18(K20( the carrier of (X), the carrier of (X)), the carrier of (X)) Element of K19(K20(K20( the carrier of (X), the carrier of (X)), the carrier of (X)))
K20( the carrier of (X), the carrier of (X)) is non empty set
K20(K20( the carrier of (X), the carrier of (X)), the carrier of (X)) is non empty set
K19(K20(K20( the carrier of (X), the carrier of (X)), the carrier of (X))) is non empty set
the L_meet of (X) . (Y,A1) is Element of the carrier of (X)
(Y "/\" A1) "\/" A1 is Element of the carrier of (X)
the L_join of (X) is V1() V4(K20( the carrier of (X), the carrier of (X))) V5( the carrier of (X)) V6() V18(K20( the carrier of (X), the carrier of (X)), the carrier of (X)) Element of K19(K20(K20( the carrier of (X), the carrier of (X)), the carrier of (X)))
the L_join of (X) . ((Y "/\" A1),A1) is Element of the carrier of (X)
(X) is non empty set
A2 is non empty (X)
a9 is non empty (X)
(X,A2,a9) is non empty (X)
INTERSECTION (A2,a9) is set
f is non empty (X)
the L_join of (X) . (f,A1) is set
(X,f,a9) is non empty (X)
UNION (f,a9) is set
the carrier of (X) is non empty set
Y is Element of the carrier of (X)
A1 is Element of the carrier of (X)
A2 is Element of the carrier of (X)
A1 "/\" A2 is Element of the carrier of (X)
the L_meet of (X) is V1() V4(K20( the carrier of (X), the carrier of (X))) V5( the carrier of (X)) V6() V18(K20( the carrier of (X), the carrier of (X)), the carrier of (X)) Element of K19(K20(K20( the carrier of (X), the carrier of (X)), the carrier of (X)))
K20( the carrier of (X), the carrier of (X)) is non empty set
K20(K20( the carrier of (X), the carrier of (X)), the carrier of (X)) is non empty set
K19(K20(K20( the carrier of (X), the carrier of (X)), the carrier of (X))) is non empty set
the L_meet of (X) . (A1,A2) is Element of the carrier of (X)
Y "/\" (A1 "/\" A2) is Element of the carrier of (X)
the L_meet of (X) . (Y,(A1 "/\" A2)) is Element of the carrier of (X)
Y "/\" A1 is Element of the carrier of (X)
the L_meet of (X) . (Y,A1) is Element of the carrier of (X)
(Y "/\" A1) "/\" A2 is Element of the carrier of (X)
the L_meet of (X) . ((Y "/\" A1),A2) is Element of the carrier of (X)
(X) is non empty set
f is non empty (X)
f is non empty (X)
(X,f,f) is non empty (X)
INTERSECTION (f,f) is set
a9 is non empty (X)
(X,a9,f) is non empty (X)
INTERSECTION (a9,f) is set
g is non empty (X)
g is non empty (X)
the L_meet of (X) . (Y,g) is set
(X,a9,g) is non empty (X)
INTERSECTION (a9,g) is set
(X,(X,a9,f),f) is non empty (X)
INTERSECTION ((X,a9,f),f) is set
the L_meet of (X) . (g,f) is set
the carrier of (X) is non empty set
Y is Element of the carrier of (X)
A1 is Element of the carrier of (X)
Y "\/" A1 is Element of the carrier of (X)
the L_join of (X) is V1() V4(K20( the carrier of (X), the carrier of (X))) V5( the carrier of (X)) V6() V18(K20( the carrier of (X), the carrier of (X)), the carrier of (X)) Element of K19(K20(K20( the carrier of (X), the carrier of (X)), the carrier of (X)))
K20( the carrier of (X), the carrier of (X)) is non empty set
K20(K20( the carrier of (X), the carrier of (X)), the carrier of (X)) is non empty set
K19(K20(K20( the carrier of (X), the carrier of (X)), the carrier of (X))) is non empty set
the L_join of (X) . (Y,A1) is Element of the carrier of (X)
Y "/\" (Y "\/" A1) is Element of the carrier of (X)
the L_meet of (X) is V1() V4(K20( the carrier of (X), the carrier of (X))) V5( the carrier of (X)) V6() V18(K20( the carrier of (X), the carrier of (X)), the carrier of (X)) Element of K19(K20(K20( the carrier of (X), the carrier of (X)), the carrier of (X)))
the L_meet of (X) . (Y,(Y "\/" A1)) is Element of the carrier of (X)
(X) is non empty set
A2 is non empty (X)
a9 is non empty (X)
(X,A2,a9) is non empty (X)
UNION (A2,a9) is set
f is non empty (X)
the L_meet of (X) . (A2,(X,A2,a9)) is set
(X,A2,f) is non empty (X)
INTERSECTION (A2,f) is set
the carrier of (X) is non empty set
Y is Element of the carrier of (X)
A1 is Element of the carrier of (X)
Y "/\" A1 is Element of the carrier of (X)
the L_meet of (X) is V1() V4(K20( the carrier of (X), the carrier of (X))) V5( the carrier of (X)) V6() V18(K20( the carrier of (X), the carrier of (X)), the carrier of (X)) Element of K19(K20(K20( the carrier of (X), the carrier of (X)), the carrier of (X)))
K20( the carrier of (X), the carrier of (X)) is non empty set
K20(K20( the carrier of (X), the carrier of (X)), the carrier of (X)) is non empty set
K19(K20(K20( the carrier of (X), the carrier of (X)), the carrier of (X))) is non empty set
the L_meet of (X) . (Y,A1) is Element of the carrier of (X)
A1 "/\" Y is Element of the carrier of (X)
the L_meet of (X) . (A1,Y) is Element of the carrier of (X)
(X) is non empty set
A2 is non empty (X)
a9 is non empty (X)
(X,A2,a9) is non empty (X)
INTERSECTION (A2,a9) is set
(X,a9,A2) is non empty (X)
INTERSECTION (a9,A2) is set
X is non empty with_tolerance L6()
the carrier of X is non empty set
K19( the carrier of X) is non empty set
K20(K19( the carrier of X),K19( the carrier of X)) is non empty set
bool the carrier of X is non empty Element of K19(K19( the carrier of X))
K19(K19( the carrier of X)) is non empty set
[:(bool the carrier of X),(bool the carrier of X):] is V1() V4(K19( the carrier of X)) V5(K19( the carrier of X)) non empty Element of K19(K20(K19( the carrier of X),K19( the carrier of X)))
K19(K20(K19( the carrier of X),K19( the carrier of X))) is non empty set
X is non empty with_tolerance L6()
the carrier of X is non empty set
K19( the carrier of X) is non empty set
Y is (X)
bool the carrier of X is non empty Element of K19(K19( the carrier of X))
K19(K19( the carrier of X)) is non empty set
A1 is set
A2 is set
[A1,A2] is V15() set
{A1,A2} is non empty set
{A1} is non empty set
{{A1,A2},{A1}} is non empty set
a9 is Element of K19( the carrier of X)
f is Element of K19( the carrier of X)
[a9,f] is V15() set
{a9,f} is non empty set
{a9} is non empty set
{{a9,f},{a9}} is non empty set
X is non empty with_tolerance L6()
the carrier of X is non empty set
K19( the carrier of X) is non empty set
Y is Element of K19( the carrier of X)
LAp Y is Element of K19( the carrier of X)
UAp Y is Element of K19( the carrier of X)
[(LAp Y),(UAp Y)] is V15() set
{(LAp Y),(UAp Y)} is non empty set
{(LAp Y)} is non empty set
{{(LAp Y),(UAp Y)},{(LAp Y)}} is non empty set
bool the carrier of X is non empty Element of K19(K19( the carrier of X))
K19(K19( the carrier of X)) is non empty set
[:(bool the carrier of X),(bool the carrier of X):] is V1() V4(K19( the carrier of X)) V5(K19( the carrier of X)) non empty Element of K19(K20(K19( the carrier of X),K19( the carrier of X)))
K20(K19( the carrier of X),K19( the carrier of X)) is non empty set
K19(K20(K19( the carrier of X),K19( the carrier of X))) is non empty set
X is non empty with_tolerance L6()
Y is (X)
Y `1 is set
the carrier of X is non empty set
K19( the carrier of X) is non empty set
A1 is Element of K19( the carrier of X)
A2 is Element of K19( the carrier of X)
[A1,A2] is V15() set
{A1,A2} is non empty set
{A1} is non empty set
{{A1,A2},{A1}} is non empty set
Y `2 is set
A1 is Element of K19( the carrier of X)
A2 is Element of K19( the carrier of X)
[A1,A2] is V15() set
{A1,A2} is non empty set
{A1} is non empty set
{{A1,A2},{A1}} is non empty set
X is non empty with_tolerance L6()
Y is (X)
A1 is (X)
(X,Y) is Element of K19( the carrier of X)
the carrier of X is non empty set
K19( the carrier of X) is non empty set
Y `1 is set
(X,A1) is Element of K19( the carrier of X)
A1 `1 is set
(X,Y) is Element of K19( the carrier of X)
Y `2 is set
(X,A1) is Element of K19( the carrier of X)
A1 `2 is set
A2 is Element of K19( the carrier of X)
a9 is Element of K19( the carrier of X)
[A2,a9] is V15() set
{A2,a9} is non empty set
{A2} is non empty set
{{A2,a9},{A2}} is non empty set
f is Element of K19( the carrier of X)
f is Element of K19( the carrier of X)
[f,f] is V15() set
{f,f} is non empty set
{f} is non empty set
{{f,f},{f}} is non empty set
X is non empty with_tolerance L6()
the carrier of X is non empty set
Y is (X)
(X,Y) is Element of K19( the carrier of X)
K19( the carrier of X) is non empty set
Y `1 is set
A1 is (X)
(X,A1) is Element of K19( the carrier of X)
A1 `1 is set
(X,Y) \/ (X,A1) is Element of K19( the carrier of X)
(X,Y) is Element of K19( the carrier of X)
Y `2 is set
(X,A1) is Element of K19( the carrier of X)
A1 `2 is set
(X,Y) \/ (X,A1) is Element of K19( the carrier of X)
[((X,Y) \/ (X,A1)),((X,Y) \/ (X,A1))] is V15() set
{((X,Y) \/ (X,A1)),((X,Y) \/ (X,A1))} is non empty set
{((X,Y) \/ (X,A1))} is non empty set
{{((X,Y) \/ (X,A1)),((X,Y) \/ (X,A1))},{((X,Y) \/ (X,A1))}} is non empty set
bool the carrier of X is non empty Element of K19(K19( the carrier of X))
K19(K19( the carrier of X)) is non empty set
[:(bool the carrier of X),(bool the carrier of X):] is V1() V4(K19( the carrier of X)) V5(K19( the carrier of X)) non empty Element of K19(K20(K19( the carrier of X),K19( the carrier of X)))
K20(K19( the carrier of X),K19( the carrier of X)) is non empty set
K19(K20(K19( the carrier of X),K19( the carrier of X))) is non empty set
(X,Y) /\ (X,A1) is Element of K19( the carrier of X)
(X,Y) /\ (X,A1) is Element of K19( the carrier of X)
[((X,Y) /\ (X,A1)),((X,Y) /\ (X,A1))] is V15() set
{((X,Y) /\ (X,A1)),((X,Y) /\ (X,A1))} is non empty set
{((X,Y) /\ (X,A1))} is non empty set
{{((X,Y) /\ (X,A1)),((X,Y) /\ (X,A1))},{((X,Y) /\ (X,A1))}} is non empty set
bool the carrier of X is non empty Element of K19(K19( the carrier of X))
K19(K19( the carrier of X)) is non empty set
[:(bool the carrier of X),(bool the carrier of X):] is V1() V4(K19( the carrier of X)) V5(K19( the carrier of X)) non empty Element of K19(K20(K19( the carrier of X),K19( the carrier of X)))
K20(K19( the carrier of X),K19( the carrier of X)) is non empty set
K19(K20(K19( the carrier of X),K19( the carrier of X))) is non empty set
X is non empty with_tolerance L6()
Y is (X)
A1 is (X)
(X,Y,A1) is (X)
the carrier of X is non empty set
(X,Y) is Element of K19( the carrier of X)
K19( the carrier of X) is non empty set
Y `1 is set
(X,A1) is Element of K19( the carrier of X)
A1 `1 is set
(X,Y) \/ (X,A1) is Element of K19( the carrier of X)
(X,Y) is Element of K19( the carrier of X)
Y `2 is set
(X,A1) is Element of K19( the carrier of X)
A1 `2 is set
(X,Y) \/ (X,A1) is Element of K19( the carrier of X)
[((X,Y) \/ (X,A1)),((X,Y) \/ (X,A1))] is V15() set
{((X,Y) \/ (X,A1)),((X,Y) \/ (X,A1))} is non empty set
{((X,Y) \/ (X,A1))} is non empty set
{{((X,Y) \/ (X,A1)),((X,Y) \/ (X,A1))},{((X,Y) \/ (X,A1))}} is non empty set
(X,(X,Y,A1)) is Element of K19( the carrier of X)
(X,Y,A1) `1 is set
X is non empty with_tolerance L6()
Y is (X)
A1 is (X)
(X,Y,A1) is (X)
the carrier of X is non empty set
(X,Y) is Element of K19( the carrier of X)
K19( the carrier of X) is non empty set
Y `1 is set
(X,A1) is Element of K19( the carrier of X)
A1 `1 is set
(X,Y) \/ (X,A1) is Element of K19( the carrier of X)
(X,Y) is Element of K19( the carrier of X)
Y `2 is set
(X,A1) is Element of K19( the carrier of X)
A1 `2 is set
(X,Y) \/ (X,A1) is Element of K19( the carrier of X)
[((X,Y) \/ (X,A1)),((X,Y) \/ (X,A1))] is V15() set
{((X,Y) \/ (X,A1)),((X,Y) \/ (X,A1))} is non empty set
{((X,Y) \/ (X,A1))} is non empty set
{{((X,Y) \/ (X,A1)),((X,Y) \/ (X,A1))},{((X,Y) \/ (X,A1))}} is non empty set
(X,(X,Y,A1)) is Element of K19( the carrier of X)
(X,Y,A1) `2 is set
X is non empty with_tolerance L6()
Y is (X)
A1 is (X)
(X,Y,A1) is (X)
the carrier of X is non empty set
(X,Y) is Element of K19( the carrier of X)
K19( the carrier of X) is non empty set
Y `1 is set
(X,A1) is Element of K19( the carrier of X)
A1 `1 is set
(X,Y) /\ (X,A1) is Element of K19( the carrier of X)
(X,Y) is Element of K19( the carrier of X)
Y `2 is set
(X,A1) is Element of K19( the carrier of X)
A1 `2 is set
(X,Y) /\ (X,A1) is Element of K19( the carrier of X)
[((X,Y) /\ (X,A1)),((X,Y) /\ (X,A1))] is V15() set
{((X,Y) /\ (X,A1)),((X,Y) /\ (X,A1))} is non empty set
{((X,Y) /\ (X,A1))} is non empty set
{{((X,Y) /\ (X,A1)),((X,Y) /\ (X,A1))},{((X,Y) /\ (X,A1))}} is non empty set
(X,(X,Y,A1)) is Element of K19( the carrier of X)
(X,Y,A1) `1 is set
X is non empty with_tolerance L6()
Y is (X)
A1 is (X)
(X,Y,A1) is (X)
the carrier of X is non empty set
(X,Y) is Element of K19( the carrier of X)
K19( the carrier of X) is non empty set
Y `1 is set
(X,A1) is Element of K19( the carrier of X)
A1 `1 is set
(X,Y) /\ (X,A1) is Element of K19( the carrier of X)
(X,Y) is Element of K19( the carrier of X)
Y `2 is set
(X,A1) is Element of K19( the carrier of X)
A1 `2 is set
(X,Y) /\ (X,A1) is Element of K19( the carrier of X)
[((X,Y) /\ (X,A1)),((X,Y) /\ (X,A1))] is V15() set
{((X,Y) /\ (X,A1)),((X,Y) /\ (X,A1))} is non empty set
{((X,Y) /\ (X,A1))} is non empty set
{{((X,Y) /\ (X,A1)),((X,Y) /\ (X,A1))},{((X,Y) /\ (X,A1))}} is non empty set
(X,(X,Y,A1)) is Element of K19( the carrier of X)
(X,Y,A1) `2 is set
X is non empty with_tolerance L6()
Y is (X)
(X,Y,Y) is (X)
the carrier of X is non empty set
(X,Y) is Element of K19( the carrier of X)
K19( the carrier of X) is non empty set
Y `1 is set
(X,Y) \/ (X,Y) is Element of K19( the carrier of X)
(X,Y) is Element of K19( the carrier of X)
Y `2 is set
(X,Y) \/ (X,Y) is Element of K19( the carrier of X)
[((X,Y) \/ (X,Y)),((X,Y) \/ (X,Y))] is V15() set
{((X,Y) \/ (X,Y)),((X,Y) \/ (X,Y))} is non empty set
{((X,Y) \/ (X,Y))} is non empty set
{{((X,Y) \/ (X,Y)),((X,Y) \/ (X,Y))},{((X,Y) \/ (X,Y))}} is non empty set
(X,(X,Y,Y)) is Element of K19( the carrier of X)
(X,Y,Y) `1 is set
(X,(X,Y,Y)) is Element of K19( the carrier of X)
(X,Y,Y) `2 is set
X is non empty with_tolerance L6()
Y is (X)
(X,Y,Y) is (X)
the carrier of X is non empty set
(X,Y) is Element of K19( the carrier of X)
K19( the carrier of X) is non empty set
Y `1 is set
(X,Y) /\ (X,Y) is Element of K19( the carrier of X)
(X,Y) is Element of K19( the carrier of X)
Y `2 is set
(X,Y) /\ (X,Y) is Element of K19( the carrier of X)
[((X,Y) /\ (X,Y)),((X,Y) /\ (X,Y))] is V15() set
{((X,Y) /\ (X,Y)),((X,Y) /\ (X,Y))} is non empty set
{((X,Y) /\ (X,Y))} is non empty set
{{((X,Y) /\ (X,Y)),((X,Y) /\ (X,Y))},{((X,Y) /\ (X,Y))}} is non empty set
(X,(X,Y,Y)) is Element of K19( the carrier of X)
(X,Y,Y) `1 is set
(X,(X,Y,Y)) is Element of K19( the carrier of X)
(X,Y,Y) `2 is set
X is non empty with_tolerance L6()
Y is (X)
A1 is (X)
(X,Y,A1) is (X)
the carrier of X is non empty set
(X,Y) is Element of K19( the carrier of X)
K19( the carrier of X) is non empty set
Y `1 is set
(X,A1) is Element of K19( the carrier of X)
A1 `1 is set
(X,Y) \/ (X,A1) is Element of K19( the carrier of X)
(X,Y) is Element of K19( the carrier of X)
Y `2 is set
(X,A1) is Element of K19( the carrier of X)
A1 `2 is set
(X,Y) \/ (X,A1) is Element of K19( the carrier of X)
[((X,Y) \/ (X,A1)),((X,Y) \/ (X,A1))] is V15() set
{((X,Y) \/ (X,A1)),((X,Y) \/ (X,A1))} is non empty set
{((X,Y) \/ (X,A1))} is non empty set
{{((X,Y) \/ (X,A1)),((X,Y) \/ (X,A1))},{((X,Y) \/ (X,A1))}} is non empty set
(X,A1,Y) is (X)
(X,A1) \/ (X,Y) is Element of K19( the carrier of X)
(X,A1) \/ (X,Y) is Element of K19( the carrier of X)
[((X,A1) \/ (X,Y)),((X,A1) \/ (X,Y))] is V15() set
{((X,A1) \/ (X,Y)),((X,A1) \/ (X,Y))} is non empty set
{((X,A1) \/ (X,Y))} is non empty set
{{((X,A1) \/ (X,Y)),((X,A1) \/ (X,Y))},{((X,A1) \/ (X,Y))}} is non empty set
X is non empty with_tolerance L6()
Y is (X)
A1 is (X)
(X,Y,A1) is (X)
the carrier of X is non empty set
(X,Y) is Element of K19( the carrier of X)
K19( the carrier of X) is non empty set
Y `1 is set
(X,A1) is Element of K19( the carrier of X)
A1 `1 is set
(X,Y) /\ (X,A1) is Element of K19( the carrier of X)
(X,Y) is Element of K19( the carrier of X)
Y `2 is set
(X,A1) is Element of K19( the carrier of X)
A1 `2 is set
(X,Y) /\ (X,A1) is Element of K19( the carrier of X)
[((X,Y) /\ (X,A1)),((X,Y) /\ (X,A1))] is V15() set
{((X,Y) /\ (X,A1)),((X,Y) /\ (X,A1))} is non empty set
{((X,Y) /\ (X,A1))} is non empty set
{{((X,Y) /\ (X,A1)),((X,Y) /\ (X,A1))},{((X,Y) /\ (X,A1))}} is non empty set
(X,A1,Y) is (X)
(X,A1) /\ (X,Y) is Element of K19( the carrier of X)
(X,A1) /\ (X,Y) is Element of K19( the carrier of X)
[((X,A1) /\ (X,Y)),((X,A1) /\ (X,Y))] is V15() set
{((X,A1) /\ (X,Y)),((X,A1) /\ (X,Y))} is non empty set
{((X,A1) /\ (X,Y))} is non empty set
{{((X,A1) /\ (X,Y)),((X,A1) /\ (X,Y))},{((X,A1) /\ (X,Y))}} is non empty set
X is non empty with_tolerance L6()
Y is (X)
A1 is (X)
(X,Y,A1) is (X)
the carrier of X is non empty set
(X,Y) is Element of K19( the carrier of X)
K19( the carrier of X) is non empty set
Y `1 is set
(X,A1) is Element of K19( the carrier of X)
A1 `1 is set
(X,Y) \/ (X,A1) is Element of K19( the carrier of X)
(X,Y) is Element of K19( the carrier of X)
Y `2 is set
(X,A1) is Element of K19( the carrier of X)
A1 `2 is set
(X,Y) \/ (X,A1) is Element of K19( the carrier of X)
[((X,Y) \/ (X,A1)),((X,Y) \/ (X,A1))] is V15() set
{((X,Y) \/ (X,A1)),((X,Y) \/ (X,A1))} is non empty set
{((X,Y) \/ (X,A1))} is non empty set
{{((X,Y) \/ (X,A1)),((X,Y) \/ (X,A1))},{((X,Y) \/ (X,A1))}} is non empty set
A2 is (X)
(X,(X,Y,A1),A2) is (X)
(X,(X,Y,A1)) is Element of K19( the carrier of X)
(X,Y,A1) `1 is set
(X,A2) is Element of K19( the carrier of X)
A2 `1 is set
(X,(X,Y,A1)) \/ (X,A2) is Element of K19( the carrier of X)
(X,(X,Y,A1)) is Element of K19( the carrier of X)
(X,Y,A1) `2 is set
(X,A2) is Element of K19( the carrier of X)
A2 `2 is set
(X,(X,Y,A1)) \/ (X,A2) is Element of K19( the carrier of X)
[((X,(X,Y,A1)) \/ (X,A2)),((X,(X,Y,A1)) \/ (X,A2))] is V15() set
{((X,(X,Y,A1)) \/ (X,A2)),((X,(X,Y,A1)) \/ (X,A2))} is non empty set
{((X,(X,Y,A1)) \/ (X,A2))} is non empty set
{{((X,(X,Y,A1)) \/ (X,A2)),((X,(X,Y,A1)) \/ (X,A2))},{((X,(X,Y,A1)) \/ (X,A2))}} is non empty set
(X,A1,A2) is (X)
(X,A1) \/ (X,A2) is Element of K19( the carrier of X)
(X,A1) \/ (X,A2) is Element of K19( the carrier of X)
[((X,A1) \/ (X,A2)),((X,A1) \/ (X,A2))] is V15() set
{((X,A1) \/ (X,A2)),((X,A1) \/ (X,A2))} is non empty set
{((X,A1) \/ (X,A2))} is non empty set
{{((X,A1) \/ (X,A2)),((X,A1) \/ (X,A2))},{((X,A1) \/ (X,A2))}} is non empty set
(X,Y,(X,A1,A2)) is (X)
(X,(X,A1,A2)) is Element of K19( the carrier of X)
(X,A1,A2) `1 is set
(X,Y) \/ (X,(X,A1,A2)) is Element of K19( the carrier of X)
(X,(X,A1,A2)) is Element of K19( the carrier of X)
(X,A1,A2) `2 is set
(X,Y) \/ (X,(X,A1,A2)) is Element of K19( the carrier of X)
[((X,Y) \/ (X,(X,A1,A2))),((X,Y) \/ (X,(X,A1,A2)))] is V15() set
{((X,Y) \/ (X,(X,A1,A2))),((X,Y) \/ (X,(X,A1,A2)))} is non empty set
{((X,Y) \/ (X,(X,A1,A2)))} is non empty set
{{((X,Y) \/ (X,(X,A1,A2))),((X,Y) \/ (X,(X,A1,A2)))},{((X,Y) \/ (X,(X,A1,A2)))}} is non empty set
((X,Y) \/ (X,A1)) \/ (X,A2) is Element of K19( the carrier of X)
(X,Y) \/ ((X,A1) \/ (X,A2)) is Element of K19( the carrier of X)
(X,(X,Y,(X,A1,A2))) is Element of K19( the carrier of X)
(X,Y,(X,A1,A2)) `1 is set
(X,(X,(X,Y,A1),A2)) is Element of K19( the carrier of X)
(X,(X,Y,A1),A2) `1 is set
(X,(X,(X,Y,A1),A2)) is Element of K19( the carrier of X)
(X,(X,Y,A1),A2) `2 is set
((X,Y) \/ (X,A1)) \/ (X,A2) is Element of K19( the carrier of X)
(X,Y) \/ ((X,A1) \/ (X,A2)) is Element of K19( the carrier of X)
(X,(X,Y,(X,A1,A2))) is Element of K19( the carrier of X)
(X,Y,(X,A1,A2)) `2 is set
X is non empty with_tolerance L6()
Y is (X)
A1 is (X)
(X,Y,A1) is (X)
the carrier of X is non empty set
(X,Y) is Element of K19( the carrier of X)
K19( the carrier of X) is non empty set
Y `1 is set
(X,A1) is Element of K19( the carrier of X)
A1 `1 is set
(X,Y) /\ (X,A1) is Element of K19( the carrier of X)
(X,Y) is Element of K19( the carrier of X)
Y `2 is set
(X,A1) is Element of K19( the carrier of X)
A1 `2 is set
(X,Y) /\ (X,A1) is Element of K19( the carrier of X)
[((X,Y) /\ (X,A1)),((X,Y) /\ (X,A1))] is V15() set
{((X,Y) /\ (X,A1)),((X,Y) /\ (X,A1))} is non empty set
{((X,Y) /\ (X,A1))} is non empty set
{{((X,Y) /\ (X,A1)),((X,Y) /\ (X,A1))},{((X,Y) /\ (X,A1))}} is non empty set
A2 is (X)
(X,(X,Y,A1),A2) is (X)
(X,(X,Y,A1)) is Element of K19( the carrier of X)
(X,Y,A1) `1 is set
(X,A2) is Element of K19( the carrier of X)
A2 `1 is set
(X,(X,Y,A1)) /\ (X,A2) is Element of K19( the carrier of X)
(X,(X,Y,A1)) is Element of K19( the carrier of X)
(X,Y,A1) `2 is set
(X,A2) is Element of K19( the carrier of X)
A2 `2 is set
(X,(X,Y,A1)) /\ (X,A2) is Element of K19( the carrier of X)
[((X,(X,Y,A1)) /\ (X,A2)),((X,(X,Y,A1)) /\ (X,A2))] is V15() set
{((X,(X,Y,A1)) /\ (X,A2)),((X,(X,Y,A1)) /\ (X,A2))} is non empty set
{((X,(X,Y,A1)) /\ (X,A2))} is non empty set
{{((X,(X,Y,A1)) /\ (X,A2)),((X,(X,Y,A1)) /\ (X,A2))},{((X,(X,Y,A1)) /\ (X,A2))}} is non empty set
(X,A1,A2) is (X)
(X,A1) /\ (X,A2) is Element of K19( the carrier of X)
(X,A1) /\ (X,A2) is Element of K19( the carrier of X)
[((X,A1) /\ (X,A2)),((X,A1) /\ (X,A2))] is V15() set
{((X,A1) /\ (X,A2)),((X,A1) /\ (X,A2))} is non empty set
{((X,A1) /\ (X,A2))} is non empty set
{{((X,A1) /\ (X,A2)),((X,A1) /\ (X,A2))},{((X,A1) /\ (X,A2))}} is non empty set
(X,Y,(X,A1,A2)) is (X)
(X,(X,A1,A2)) is Element of K19( the carrier of X)
(X,A1,A2) `1 is set
(X,Y) /\ (X,(X,A1,A2)) is Element of K19( the carrier of X)
(X,(X,A1,A2)) is Element of K19( the carrier of X)
(X,A1,A2) `2 is set
(X,Y) /\ (X,(X,A1,A2)) is Element of K19( the carrier of X)
[((X,Y) /\ (X,(X,A1,A2))),((X,Y) /\ (X,(X,A1,A2)))] is V15() set
{((X,Y) /\ (X,(X,A1,A2))),((X,Y) /\ (X,(X,A1,A2)))} is non empty set
{((X,Y) /\ (X,(X,A1,A2)))} is non empty set
{{((X,Y) /\ (X,(X,A1,A2))),((X,Y) /\ (X,(X,A1,A2)))},{((X,Y) /\ (X,(X,A1,A2)))}} is non empty set
((X,Y) /\ (X,A1)) /\ (X,A2) is Element of K19( the carrier of X)
(X,Y) /\ ((X,A1) /\ (X,A2)) is Element of K19( the carrier of X)
((X,Y) /\ (X,A1)) /\ (X,A2) is Element of K19( the carrier of X)
(X,Y) /\ ((X,A1) /\ (X,A2)) is Element of K19( the carrier of X)
X is non empty with_tolerance L6()
Y is (X)
A1 is (X)
(X,Y,A1) is (X)
the carrier of X is non empty set
(X,Y) is Element of K19( the carrier of X)
K19( the carrier of X) is non empty set
Y `1 is set
(X,A1) is Element of K19( the carrier of X)
A1 `1 is set
(X,Y) /\ (X,A1) is Element of K19( the carrier of X)
(X,Y) is Element of K19( the carrier of X)
Y `2 is set
(X,A1) is Element of K19( the carrier of X)
A1 `2 is set
(X,Y) /\ (X,A1) is Element of K19( the carrier of X)
[((X,Y) /\ (X,A1)),((X,Y) /\ (X,A1))] is V15() set
{((X,Y) /\ (X,A1)),((X,Y) /\ (X,A1))} is non empty set
{((X,Y) /\ (X,A1))} is non empty set
{{((X,Y) /\ (X,A1)),((X,Y) /\ (X,A1))},{((X,Y) /\ (X,A1))}} is non empty set
A2 is (X)
(X,A1,A2) is (X)
(X,A2) is Element of K19( the carrier of X)
A2 `1 is set
(X,A1) \/ (X,A2) is Element of K19( the carrier of X)
(X,A2) is Element of K19( the carrier of X)
A2 `2 is set
(X,A1) \/ (X,A2) is Element of K19( the carrier of X)
[((X,A1) \/ (X,A2)),((X,A1) \/ (X,A2))] is V15() set
{((X,A1) \/ (X,A2)),((X,A1) \/ (X,A2))} is non empty set
{((X,A1) \/ (X,A2))} is non empty set
{{((X,A1) \/ (X,A2)),((X,A1) \/ (X,A2))},{((X,A1) \/ (X,A2))}} is non empty set
(X,Y,(X,A1,A2)) is (X)
(X,(X,A1,A2)) is Element of K19( the carrier of X)
(X,A1,A2) `1 is set
(X,Y) /\ (X,(X,A1,A2)) is Element of K19( the carrier of X)
(X,(X,A1,A2)) is Element of K19( the carrier of X)
(X,A1,A2) `2 is set
(X,Y) /\ (X,(X,A1,A2)) is Element of K19( the carrier of X)
[((X,Y) /\ (X,(X,A1,A2))),((X,Y) /\ (X,(X,A1,A2)))] is V15() set
{((X,Y) /\ (X,(X,A1,A2))),((X,Y) /\ (X,(X,A1,A2)))} is non empty set
{((X,Y) /\ (X,(X,A1,A2)))} is non empty set
{{((X,Y) /\ (X,(X,A1,A2))),((X,Y) /\ (X,(X,A1,A2)))},{((X,Y) /\ (X,(X,A1,A2)))}} is non empty set
(X,Y,A2) is (X)
(X,Y) /\ (X,A2) is Element of K19( the carrier of X)
(X,Y) /\ (X,A2) is Element of K19( the carrier of X)
[((X,Y) /\ (X,A2)),((X,Y) /\ (X,A2))] is V15() set
{((X,Y) /\ (X,A2)),((X,Y) /\ (X,A2))} is non empty set
{((X,Y) /\ (X,A2))} is non empty set
{{((X,Y) /\ (X,A2)),((X,Y) /\ (X,A2))},{((X,Y) /\ (X,A2))}} is non empty set
(X,(X,Y,A1),(X,Y,A2)) is (X)
(X,(X,Y,A1)) is Element of K19( the carrier of X)
(X,Y,A1) `1 is set
(X,(X,Y,A2)) is Element of K19( the carrier of X)
(X,Y,A2) `1 is set
(X,(X,Y,A1)) \/ (X,(X,Y,A2)) is Element of K19( the carrier of X)
(X,(X,Y,A1)) is Element of K19( the carrier of X)
(X,Y,A1) `2 is set
(X,(X,Y,A2)) is Element of K19( the carrier of X)
(X,Y,A2) `2 is set
(X,(X,Y,A1)) \/ (X,(X,Y,A2)) is Element of K19( the carrier of X)
[((X,(X,Y,A1)) \/ (X,(X,Y,A2))),((X,(X,Y,A1)) \/ (X,(X,Y,A2)))] is V15() set
{((X,(X,Y,A1)) \/ (X,(X,Y,A2))),((X,(X,Y,A1)) \/ (X,(X,Y,A2)))} is non empty set
{((X,(X,Y,A1)) \/ (X,(X,Y,A2)))} is non empty set
{{((X,(X,Y,A1)) \/ (X,(X,Y,A2))),((X,(X,Y,A1)) \/ (X,(X,Y,A2)))},{((X,(X,Y,A1)) \/ (X,(X,Y,A2)))}} is non empty set
(X,(X,Y,(X,A1,A2))) is Element of K19( the carrier of X)
(X,Y,(X,A1,A2)) `1 is set
(X,Y) /\ ((X,A1) \/ (X,A2)) is Element of K19( the carrier of X)
((X,Y) /\ (X,A1)) \/ ((X,Y) /\ (X,A2)) is Element of K19( the carrier of X)
(X,(X,Y,A1)) \/ ((X,Y) /\ (X,A2)) is Element of K19( the carrier of X)
(X,(X,(X,Y,A1),(X,Y,A2))) is Element of K19( the carrier of X)
(X,(X,Y,A1),(X,Y,A2)) `1 is set
(X,(X,Y,(X,A1,A2))) is Element of K19( the carrier of X)
(X,Y,(X,A1,A2)) `2 is set
(X,Y) /\ ((X,A1) \/ (X,A2)) is Element of K19( the carrier of X)
((X,Y) /\ (X,A1)) \/ ((X,Y) /\ (X,A2)) is Element of K19( the carrier of X)
(X,(X,Y,A1)) \/ ((X,Y) /\ (X,A2)) is Element of K19( the carrier of X)
(X,(X,(X,Y,A1),(X,Y,A2))) is Element of K19( the carrier of X)
(X,(X,Y,A1),(X,Y,A2)) `2 is set
X is non empty with_tolerance L6()
Y is (X)
A1 is (X)
(X,Y,A1) is (X)
the carrier of X is non empty set
(X,Y) is Element of K19( the carrier of X)
K19( the carrier of X) is non empty set
Y `1 is set
(X,A1) is Element of K19( the carrier of X)
A1 `1 is set
(X,Y) /\ (X,A1) is Element of K19( the carrier of X)
(X,Y) is Element of K19( the carrier of X)
Y `2 is set
(X,A1) is Element of K19( the carrier of X)
A1 `2 is set
(X,Y) /\ (X,A1) is Element of K19( the carrier of X)
[((X,Y) /\ (X,A1)),((X,Y) /\ (X,A1))] is V15() set
{((X,Y) /\ (X,A1)),((X,Y) /\ (X,A1))} is non empty set
{((X,Y) /\ (X,A1))} is non empty set
{{((X,Y) /\ (X,A1)),((X,Y) /\ (X,A1))},{((X,Y) /\ (X,A1))}} is non empty set
(X,Y,(X,Y,A1)) is (X)
(X,(X,Y,A1)) is Element of K19( the carrier of X)
(X,Y,A1) `1 is set
(X,Y) \/ (X,(X,Y,A1)) is Element of K19( the carrier of X)
(X,(X,Y,A1)) is Element of K19( the carrier of X)
(X,Y,A1) `2 is set
(X,Y) \/ (X,(X,Y,A1)) is Element of K19( the carrier of X)
[((X,Y) \/ (X,(X,Y,A1))),((X,Y) \/ (X,(X,Y,A1)))] is V15() set
{((X,Y) \/ (X,(X,Y,A1))),((X,Y) \/ (X,(X,Y,A1)))} is non empty set
{((X,Y) \/ (X,(X,Y,A1)))} is non empty set
{{((X,Y) \/ (X,(X,Y,A1))),((X,Y) \/ (X,(X,Y,A1)))},{((X,Y) \/ (X,(X,Y,A1)))}} is non empty set
(X,(X,Y,(X,Y,A1))) is Element of K19( the carrier of X)
(X,Y,(X,Y,A1)) `1 is set
(X,Y) \/ ((X,Y) /\ (X,A1)) is Element of K19( the carrier of X)
(X,(X,Y,(X,Y,A1))) is Element of K19( the carrier of X)
(X,Y,(X,Y,A1)) `2 is set
(X,Y) \/ ((X,Y) /\ (X,A1)) is Element of K19( the carrier of X)
X is non empty with_tolerance L6()
Y is (X)
A1 is (X)
(X,Y,A1) is (X)
the carrier of X is non empty set
(X,Y) is Element of K19( the carrier of X)
K19( the carrier of X) is non empty set
Y `1 is set
(X,A1) is Element of K19( the carrier of X)
A1 `1 is set
(X,Y) \/ (X,A1) is Element of K19( the carrier of X)
(X,Y) is Element of K19( the carrier of X)
Y `2 is set
(X,A1) is Element of K19( the carrier of X)
A1 `2 is set
(X,Y) \/ (X,A1) is Element of K19( the carrier of X)
[((X,Y) \/ (X,A1)),((X,Y) \/ (X,A1))] is V15() set
{((X,Y) \/ (X,A1)),((X,Y) \/ (X,A1))} is non empty set
{((X,Y) \/ (X,A1))} is non empty set
{{((X,Y) \/ (X,A1)),((X,Y) \/ (X,A1))},{((X,Y) \/ (X,A1))}} is non empty set
(X,Y,(X,Y,A1)) is (X)
(X,(X,Y,A1)) is Element of K19( the carrier of X)
(X,Y,A1) `1 is set
(X,Y) /\ (X,(X,Y,A1)) is Element of K19( the carrier of X)
(X,(X,Y,A1)) is Element of K19( the carrier of X)
(X,Y,A1) `2 is set
(X,Y) /\ (X,(X,Y,A1)) is Element of K19( the carrier of X)
[((X,Y) /\ (X,(X,Y,A1))),((X,Y) /\ (X,(X,Y,A1)))] is V15() set
{((X,Y) /\ (X,(X,Y,A1))),((X,Y) /\ (X,(X,Y,A1)))} is non empty set
{((X,Y) /\ (X,(X,Y,A1)))} is non empty set
{{((X,Y) /\ (X,(X,Y,A1))),((X,Y) /\ (X,(X,Y,A1)))},{((X,Y) /\ (X,(X,Y,A1)))}} is non empty set
(X,(X,Y,(X,Y,A1))) is Element of K19( the carrier of X)
(X,Y,(X,Y,A1)) `1 is set
(X,Y) /\ ((X,Y) \/ (X,A1)) is Element of K19( the carrier of X)
(X,(X,Y,(X,Y,A1))) is Element of K19( the carrier of X)
(X,Y,(X,Y,A1)) `2 is set
(X,Y) /\ ((X,Y) \/ (X,A1)) is Element of K19( the carrier of X)
X is non empty with_tolerance L6()
the carrier of X is non empty set
K19( the carrier of X) is non empty set
bool the carrier of X is non empty Element of K19(K19( the carrier of X))
K19(K19( the carrier of X)) is non empty set
[:(bool the carrier of X),(bool the carrier of X):] is V1() V4(K19( the carrier of X)) V5(K19( the carrier of X)) non empty Element of K19(K20(K19( the carrier of X),K19( the carrier of X)))
K20(K19( the carrier of X),K19( the carrier of X)) is non empty set
K19(K20(K19( the carrier of X),K19( the carrier of X))) is non empty set
Y is set
A1 is set
Y is set
A1 is set
A2 is set
X is non empty with_tolerance L6()
(X) is set
the (X) is (X)
X is non empty with_tolerance L6()
(X) is non empty set
Y is Element of (X)
X is non empty with_tolerance L6()
Y is (X)
(X) is non empty set
X is non empty with_tolerance L6()
(X) is non empty set
K20((X),(X)) is non empty set
K20(K20((X),(X)),(X)) is non empty set
K19(K20(K20((X),(X)),(X))) is non empty set
Y is V1() V4(K20((X),(X))) V5((X)) V6() V18(K20((X),(X)),(X)) Element of K19(K20(K20((X),(X)),(X)))
A1 is V1() V4(K20((X),(X))) V5((X)) V6() V18(K20((X),(X)),(X)) Element of K19(K20(K20((X),(X)),(X)))
LattStr(# (X),Y,A1 #) is non empty strict LattStr
A2 is non empty strict LattStr
the carrier of A2 is non empty set
the L_join of A2 is V1() V4(K20( the carrier of A2, the carrier of A2)) V5( the carrier of A2) V6() V18(K20( the carrier of A2, the carrier of A2), the carrier of A2) Element of K19(K20(K20( the carrier of A2, the carrier of A2), the carrier of A2))
K20( the carrier of A2, the carrier of A2) is non empty set
K20(K20( the carrier of A2, the carrier of A2), the carrier of A2) is non empty set
K19(K20(K20( the carrier of A2, the carrier of A2), the carrier of A2)) is non empty set
the L_meet of A2 is V1() V4(K20( the carrier of A2, the carrier of A2)) V5( the carrier of A2) V6() V18(K20( the carrier of A2, the carrier of A2), the carrier of A2) Element of K19(K20(K20( the carrier of A2, the carrier of A2), the carrier of A2))
a9 is Element of (X)
f is Element of (X)
the L_join of A2 . (a9,f) is set
the L_meet of A2 . (a9,f) is set
f is (X)
g is (X)
(X,f,g) is (X)
the carrier of X is non empty set
(X,f) is Element of K19( the carrier of X)
K19( the carrier of X) is non empty set
f `1 is set
(X,g) is Element of K19( the carrier of X)
g `1 is set
(X,f) \/ (X,g) is Element of K19( the carrier of X)
(X,f) is Element of K19( the carrier of X)
f `2 is set
(X,g) is Element of K19( the carrier of X)
g `2 is set
(X,f) \/ (X,g) is Element of K19( the carrier of X)
[((X,f) \/ (X,g)),((X,f) \/ (X,g))] is V15() set
{((X,f) \/ (X,g)),((X,f) \/ (X,g))} is non empty set
{((X,f) \/ (X,g))} is non empty set
{{((X,f) \/ (X,g)),((X,f) \/ (X,g))},{((X,f) \/ (X,g))}} is non empty set
(X,f,g) is (X)
(X,f) /\ (X,g) is Element of K19( the carrier of X)
(X,f) /\ (X,g) is Element of K19( the carrier of X)
[((X,f) /\ (X,g)),((X,f) /\ (X,g))] is V15() set
{((X,f) /\ (X,g)),((X,f) /\ (X,g))} is non empty set
{((X,f) /\ (X,g))} is non empty set
{{((X,f) /\ (X,g)),((X,f) /\ (X,g))},{((X,f) /\ (X,g))}} is non empty set
(X,a9) is (X)
(X,f) is (X)
(X,(X,a9),(X,f)) is (X)
(X,(X,a9)) is Element of K19( the carrier of X)
(X,a9) `1 is set
(X,(X,f)) is Element of K19( the carrier of X)
(X,f) `1 is set
(X,(X,a9)) \/ (X,(X,f)) is Element of K19( the carrier of X)
(X,(X,a9)) is Element of K19( the carrier of X)
(X,a9) `2 is set
(X,(X,f)) is Element of K19( the carrier of X)
(X,f) `2 is set
(X,(X,a9)) \/ (X,(X,f)) is Element of K19( the carrier of X)
[((X,(X,a9)) \/ (X,(X,f))),((X,(X,a9)) \/ (X,(X,f)))] is V15() set
{((X,(X,a9)) \/ (X,(X,f))),((X,(X,a9)) \/ (X,(X,f)))} is non empty set
{((X,(X,a9)) \/ (X,(X,f)))} is non empty set
{{((X,(X,a9)) \/ (X,(X,f))),((X,(X,a9)) \/ (X,(X,f)))},{((X,(X,a9)) \/ (X,(X,f)))}} is non empty set
(X,(X,(X,a9),(X,f))) is Element of (X)
(X,(X,a9),(X,f)) is (X)
(X,(X,a9)) /\ (X,(X,f)) is Element of K19( the carrier of X)
(X,(X,a9)) /\ (X,(X,f)) is Element of K19( the carrier of X)
[((X,(X,a9)) /\ (X,(X,f))),((X,(X,a9)) /\ (X,(X,f)))] is V15() set
{((X,(X,a9)) /\ (X,(X,f))),((X,(X,a9)) /\ (X,(X,f)))} is non empty set
{((X,(X,a9)) /\ (X,(X,f)))} is non empty set
{{((X,(X,a9)) /\ (X,(X,f))),((X,(X,a9)) /\ (X,(X,f)))},{((X,(X,a9)) /\ (X,(X,f)))}} is non empty set
(X,(X,(X,a9),(X,f))) is Element of (X)
Y is strict LattStr
the carrier of Y is set
the L_join of Y is V1() V4(K20( the carrier of Y, the carrier of Y)) V5( the carrier of Y) V6() V18(K20( the carrier of Y, the carrier of Y), the carrier of Y) Element of K19(K20(K20( the carrier of Y, the carrier of Y), the carrier of Y))
K20( the carrier of Y, the carrier of Y) is set
K20(K20( the carrier of Y, the carrier of Y), the carrier of Y) is set
K19(K20(K20( the carrier of Y, the carrier of Y), the carrier of Y)) is non empty set
the L_meet of Y is V1() V4(K20( the carrier of Y, the carrier of Y)) V5( the carrier of Y) V6() V18(K20( the carrier of Y, the carrier of Y), the carrier of Y) Element of K19(K20(K20( the carrier of Y, the carrier of Y), the carrier of Y))
A1 is strict LattStr
the carrier of A1 is set
the L_join of A1 is V1() V4(K20( the carrier of A1, the carrier of A1)) V5( the carrier of A1) V6() V18(K20( the carrier of A1, the carrier of A1), the carrier of A1) Element of K19(K20(K20( the carrier of A1, the carrier of A1), the carrier of A1))
K20( the carrier of A1, the carrier of A1) is set
K20(K20( the carrier of A1, the carrier of A1), the carrier of A1) is set
K19(K20(K20( the carrier of A1, the carrier of A1), the carrier of A1)) is non empty set
the L_meet of A1 is V1() V4(K20( the carrier of A1, the carrier of A1)) V5( the carrier of A1) V6() V18(K20( the carrier of A1, the carrier of A1), the carrier of A1) Element of K19(K20(K20( the carrier of A1, the carrier of A1), the carrier of A1))
K20((X),(X)) is non empty set
K20(K20((X),(X)),(X)) is non empty set
K19(K20(K20((X),(X)),(X))) is non empty set
f is V1() V4(K20((X),(X))) V5((X)) V6() V18(K20((X),(X)),(X)) Element of K19(K20(K20((X),(X)),(X)))
g is Element of (X)
g is Element of (X)
f . (g,g) is Element of (X)
(X,g) is (X)
(X,g) is (X)
(X,(X,g),(X,g)) is (X)
the carrier of X is non empty set
(X,(X,g)) is Element of K19( the carrier of X)
K19( the carrier of X) is non empty set
(X,g) `1 is set
(X,(X,g)) is Element of K19( the carrier of X)
(X,g) `1 is set
(X,(X,g)) \/ (X,(X,g)) is Element of K19( the carrier of X)
(X,(X,g)) is Element of K19( the carrier of X)
(X,g) `2 is set
(X,(X,g)) is Element of K19( the carrier of X)
(X,g) `2 is set
(X,(X,g)) \/ (X,(X,g)) is Element of K19( the carrier of X)
[((X,(X,g)) \/ (X,(X,g))),((X,(X,g)) \/ (X,(X,g)))] is V15() set
{((X,(X,g)) \/ (X,(X,g))),((X,(X,g)) \/ (X,(X,g)))} is non empty set
{((X,(X,g)) \/ (X,(X,g)))} is non empty set
{{((X,(X,g)) \/ (X,(X,g))),((X,(X,g)) \/ (X,(X,g)))},{((X,(X,g)) \/ (X,(X,g)))}} is non empty set
f is V1() V4(K20((X),(X))) V5((X)) V6() V18(K20((X),(X)),(X)) Element of K19(K20(K20((X),(X)),(X)))
f . (g,g) is Element of (X)
A2 is V1() V4(K20((X),(X))) V5((X)) V6() V18(K20((X),(X)),(X)) Element of K19(K20(K20((X),(X)),(X)))
g is Element of (X)
g is Element of (X)
A2 . (g,g) is Element of (X)
(X,g) is (X)
(X,g) is (X)
(X,(X,g),(X,g)) is (X)
(X,(X,g)) is Element of K19( the carrier of X)
(X,g) `1 is set
(X,(X,g)) is Element of K19( the carrier of X)
(X,g) `1 is set
(X,(X,g)) /\ (X,(X,g)) is Element of K19( the carrier of X)
(X,(X,g)) is Element of K19( the carrier of X)
(X,g) `2 is set
(X,(X,g)) is Element of K19( the carrier of X)
(X,g) `2 is set
(X,(X,g)) /\ (X,(X,g)) is Element of K19( the carrier of X)
[((X,(X,g)) /\ (X,(X,g))),((X,(X,g)) /\ (X,(X,g)))] is V15() set
{((X,(X,g)) /\ (X,(X,g))),((X,(X,g)) /\ (X,(X,g)))} is non empty set
{((X,(X,g)) /\ (X,(X,g)))} is non empty set
{{((X,(X,g)) /\ (X,(X,g))),((X,(X,g)) /\ (X,(X,g)))},{((X,(X,g)) /\ (X,(X,g)))}} is non empty set
a9 is V1() V4(K20((X),(X))) V5((X)) V6() V18(K20((X),(X)),(X)) Element of K19(K20(K20((X),(X)),(X)))
a9 . (g,g) is Element of (X)
X is non empty with_tolerance L6()
(X) is strict LattStr
the carrier of (X) is set
(X) is non empty set
X is non empty with_tolerance L6()
(X) is non empty strict LattStr
the carrier of (X) is non empty set
A1 is Element of the carrier of (X)
A2 is Element of the carrier of (X)
A1 "\/" A2 is Element of the carrier of (X)
the L_join of (X) is V1() V4(K20( the carrier of (X), the carrier of (X))) V5( the carrier of (X)) V6() V18(K20( the carrier of (X), the carrier of (X)), the carrier of (X)) Element of K19(K20(K20( the carrier of (X), the carrier of (X)), the carrier of (X)))
K20( the carrier of (X), the carrier of (X)) is non empty set
K20(K20( the carrier of (X), the carrier of (X)), the carrier of (X)) is non empty set
K19(K20(K20( the carrier of (X), the carrier of (X)), the carrier of (X))) is non empty set
the L_join of (X) . (A1,A2) is Element of the carrier of (X)
A2 "\/" A1 is Element of the carrier of (X)
the L_join of (X) . (A2,A1) is Element of the carrier of (X)
(X) is non empty set
a9 is Element of (X)
f is Element of (X)
f is (X)
g is (X)
(X,f,g) is (X)
the carrier of X is non empty set
(X,f) is Element of K19( the carrier of X)
K19( the carrier of X) is non empty set
f `1 is set
(X,g) is Element of K19( the carrier of X)
g `1 is set
(X,f) \/ (X,g) is Element of K19( the carrier of X)
(X,f) is Element of K19( the carrier of X)
f `2 is set
(X,g) is Element of K19( the carrier of X)
g `2 is set
(X,f) \/ (X,g) is Element of K19( the carrier of X)
[((X,f) \/ (X,g)),((X,f) \/ (X,g))] is V15() set
{((X,f) \/ (X,g)),((X,f) \/ (X,g))} is non empty set
{((X,f) \/ (X,g))} is non empty set
{{((X,f) \/ (X,g)),((X,f) \/ (X,g))},{((X,f) \/ (X,g))}} is non empty set
(X,g,f) is (X)
(X,g) \/ (X,f) is Element of K19( the carrier of X)
(X,g) \/ (X,f) is Element of K19( the carrier of X)
[((X,g) \/ (X,f)),((X,g) \/ (X,f))] is V15() set
{((X,g) \/ (X,f)),((X,g) \/ (X,f))} is non empty set
{((X,g) \/ (X,f))} is non empty set
{{((X,g) \/ (X,f)),((X,g) \/ (X,f))},{((X,g) \/ (X,f))}} is non empty set
X is non empty with_tolerance L6()
(X) is non empty strict LattStr
the carrier of (X) is non empty set
Y is Element of the carrier of (X)
A1 is Element of the carrier of (X)
A2 is Element of the carrier of (X)
A1 "\/" A2 is Element of the carrier of (X)
the L_join of (X) is V1() V4(K20( the carrier of (X), the carrier of (X))) V5( the carrier of (X)) V6() V18(K20( the carrier of (X), the carrier of (X)), the carrier of (X)) Element of K19(K20(K20( the carrier of (X), the carrier of (X)), the carrier of (X)))
K20( the carrier of (X), the carrier of (X)) is non empty set
K20(K20( the carrier of (X), the carrier of (X)), the carrier of (X)) is non empty set
K19(K20(K20( the carrier of (X), the carrier of (X)), the carrier of (X))) is non empty set
the L_join of (X) . (A1,A2) is Element of the carrier of (X)
Y "\/" (A1 "\/" A2) is Element of the carrier of (X)
the L_join of (X) . (Y,(A1 "\/" A2)) is Element of the carrier of (X)
Y "\/" A1 is Element of the carrier of (X)
the L_join of (X) . (Y,A1) is Element of the carrier of (X)
(Y "\/" A1) "\/" A2 is Element of the carrier of (X)
the L_join of (X) . ((Y "\/" A1),A2) is Element of the carrier of (X)
(X) is non empty set
a9 is Element of (X)
f is Element of (X)
f is Element of (X)
g is (X)
a9 is (X)
(X,g,a9) is (X)
the carrier of X is non empty set
(X,g) is Element of K19( the carrier of X)
K19( the carrier of X) is non empty set
g `1 is set
(X,a9) is Element of K19( the carrier of X)
a9 `1 is set
(X,g) \/ (X,a9) is Element of K19( the carrier of X)
(X,g) is Element of K19( the carrier of X)
g `2 is set
(X,a9) is Element of K19( the carrier of X)
a9 `2 is set
(X,g) \/ (X,a9) is Element of K19( the carrier of X)
[((X,g) \/ (X,a9)),((X,g) \/ (X,a9))] is V15() set
{((X,g) \/ (X,a9)),((X,g) \/ (X,a9))} is non empty set
{((X,g) \/ (X,a9))} is non empty set
{{((X,g) \/ (X,a9)),((X,g) \/ (X,a9))},{((X,g) \/ (X,a9))}} is non empty set
g is (X)
(X,g,g) is (X)
(X,g) is Element of K19( the carrier of X)
g `1 is set
(X,g) \/ (X,g) is Element of K19( the carrier of X)
(X,g) is Element of K19( the carrier of X)
g `2 is set
(X,g) \/ (X,g) is Element of K19( the carrier of X)
[((X,g) \/ (X,g)),((X,g) \/ (X,g))] is V15() set
{((X,g) \/ (X,g)),((X,g) \/ (X,g))} is non empty set
{((X,g) \/ (X,g))} is non empty set
{{((X,g) \/ (X,g)),((X,g) \/ (X,g))},{((X,g) \/ (X,g))}} is non empty set
the L_join of (X) . (Y,(X,g,a9)) is set
(X,g,(X,g,a9)) is (X)
(X,(X,g,a9)) is Element of K19( the carrier of X)
(X,g,a9) `1 is set
(X,g) \/ (X,(X,g,a9)) is Element of K19( the carrier of X)
(X,(X,g,a9)) is Element of K19( the carrier of X)
(X,g,a9) `2 is set
(X,g) \/ (X,(X,g,a9)) is Element of K19( the carrier of X)
[((X,g) \/ (X,(X,g,a9))),((X,g) \/ (X,(X,g,a9)))] is V15() set
{((X,g) \/ (X,(X,g,a9))),((X,g) \/ (X,(X,g,a9)))} is non empty set
{((X,g) \/ (X,(X,g,a9)))} is non empty set
{{((X,g) \/ (X,(X,g,a9))),((X,g) \/ (X,(X,g,a9)))},{((X,g) \/ (X,(X,g,a9)))}} is non empty set
(X,(X,g,g),a9) is (X)
(X,(X,g,g)) is Element of K19( the carrier of X)
(X,g,g) `1 is set
(X,(X,g,g)) \/ (X,a9) is Element of K19( the carrier of X)
(X,(X,g,g)) is Element of K19( the carrier of X)
(X,g,g) `2 is set
(X,(X,g,g)) \/ (X,a9) is Element of K19( the carrier of X)
[((X,(X,g,g)) \/ (X,a9)),((X,(X,g,g)) \/ (X,a9))] is V15() set
{((X,(X,g,g)) \/ (X,a9)),((X,(X,g,g)) \/ (X,a9))} is non empty set
{((X,(X,g,g)) \/ (X,a9))} is non empty set
{{((X,(X,g,g)) \/ (X,a9)),((X,(X,g,g)) \/ (X,a9))},{((X,(X,g,g)) \/ (X,a9))}} is non empty set
the L_join of (X) . ((X,g,g),f) is set
X is non empty with_tolerance L6()
(X) is non empty set
(X) is non empty strict LattStr
the L_join of (X) is V1() V4(K20( the carrier of (X), the carrier of (X))) V5( the carrier of (X)) V6() V18(K20( the carrier of (X), the carrier of (X)), the carrier of (X)) Element of K19(K20(K20( the carrier of (X), the carrier of (X)), the carrier of (X)))
the carrier of (X) is non empty set
K20( the carrier of (X), the carrier of (X)) is non empty set
K20(K20( the carrier of (X), the carrier of (X)), the carrier of (X)) is non empty set
K19(K20(K20( the carrier of (X), the carrier of (X)), the carrier of (X))) is non empty set
the L_meet of (X) is V1() V4(K20( the carrier of (X), the carrier of (X))) V5( the carrier of (X)) V6() V18(K20( the carrier of (X), the carrier of (X)), the carrier of (X)) Element of K19(K20(K20( the carrier of (X), the carrier of (X)), the carrier of (X)))
Y is Element of (X)
A1 is Element of (X)
the L_meet of (X) . (Y,A1) is set
the L_join of (X) . (( the L_meet of (X) . (Y,A1)),A1) is set
A2 is (X)
a9 is (X)
(X,A2,a9) is (X)
the carrier of X is non empty set
(X,A2) is Element of K19( the carrier of X)
K19( the carrier of X) is non empty set
A2 `1 is set
(X,a9) is Element of K19( the carrier of X)
a9 `1 is set
(X,A2) /\ (X,a9) is Element of K19( the carrier of X)
(X,A2) is Element of K19( the carrier of X)
A2 `2 is set
(X,a9) is Element of K19( the carrier of X)
a9 `2 is set
(X,A2) /\ (X,a9) is Element of K19( the carrier of X)
[((X,A2) /\ (X,a9)),((X,A2) /\ (X,a9))] is V15() set
{((X,A2) /\ (X,a9)),((X,A2) /\ (X,a9))} is non empty set
{((X,A2) /\ (X,a9))} is non empty set
{{((X,A2) /\ (X,a9)),((X,A2) /\ (X,a9))},{((X,A2) /\ (X,a9))}} is non empty set
the L_join of (X) . ((X,A2,a9),A1) is set
(X,(X,A2,a9),a9) is (X)
(X,(X,A2,a9)) is Element of K19( the carrier of X)
(X,A2,a9) `1 is set
(X,(X,A2,a9)) \/ (X,a9) is Element of K19( the carrier of X)
(X,(X,A2,a9)) is Element of K19( the carrier of X)
(X,A2,a9) `2 is set
(X,(X,A2,a9)) \/ (X,a9) is Element of K19( the carrier of X)
[((X,(X,A2,a9)) \/ (X,a9)),((X,(X,A2,a9)) \/ (X,a9))] is V15() set
{((X,(X,A2,a9)) \/ (X,a9)),((X,(X,A2,a9)) \/ (X,a9))} is non empty set
{((X,(X,A2,a9)) \/ (X,a9))} is non empty set
{{((X,(X,A2,a9)) \/ (X,a9)),((X,(X,A2,a9)) \/ (X,a9))},{((X,(X,A2,a9)) \/ (X,a9))}} is non empty set
(X,a9,A2) is (X)
(X,a9) /\ (X,A2) is Element of K19( the carrier of X)
(X,a9) /\ (X,A2) is Element of K19( the carrier of X)
[((X,a9) /\ (X,A2)),((X,a9) /\ (X,A2))] is V15() set
{((X,a9) /\ (X,A2)),((X,a9) /\ (X,A2))} is non empty set
{((X,a9) /\ (X,A2))} is non empty set
{{((X,a9) /\ (X,A2)),((X,a9) /\ (X,A2))},{((X,a9) /\ (X,A2))}} is non empty set
(X,a9,(X,a9,A2)) is (X)
(X,(X,a9,A2)) is Element of K19( the carrier of X)
(X,a9,A2) `1 is set
(X,a9) \/ (X,(X,a9,A2)) is Element of K19( the carrier of X)
(X,(X,a9,A2)) is Element of K19( the carrier of X)
(X,a9,A2) `2 is set
(X,a9) \/ (X,(X,a9,A2)) is Element of K19( the carrier of X)
[((X,a9) \/ (X,(X,a9,A2))),((X,a9) \/ (X,(X,a9,A2)))] is V15() set
{((X,a9) \/ (X,(X,a9,A2))),((X,a9) \/ (X,(X,a9,A2)))} is non empty set
{((X,a9) \/ (X,(X,a9,A2)))} is non empty set
{{((X,a9) \/ (X,(X,a9,A2))),((X,a9) \/ (X,(X,a9,A2)))},{((X,a9) \/ (X,(X,a9,A2)))}} is non empty set
X is non empty with_tolerance L6()
(X) is non empty strict LattStr
the carrier of (X) is non empty set
Y is Element of the carrier of (X)
A1 is Element of the carrier of (X)
Y "/\" A1 is Element of the carrier of (X)
the L_meet of (X) is V1() V4(K20( the carrier of (X), the carrier of (X))) V5( the carrier of (X)) V6() V18(K20( the carrier of (X), the carrier of (X)), the carrier of (X)) Element of K19(K20(K20( the carrier of (X), the carrier of (X)), the carrier of (X)))
K20( the carrier of (X), the carrier of (X)) is non empty set
K20(K20( the carrier of (X), the carrier of (X)), the carrier of (X)) is non empty set
K19(K20(K20( the carrier of (X), the carrier of (X)), the carrier of (X))) is non empty set
the L_meet of (X) . (Y,A1) is Element of the carrier of (X)
(Y "/\" A1) "\/" A1 is Element of the carrier of (X)
the L_join of (X) is V1() V4(K20( the carrier of (X), the carrier of (X))) V5( the carrier of (X)) V6() V18(K20( the carrier of (X), the carrier of (X)), the carrier of (X)) Element of K19(K20(K20( the carrier of (X), the carrier of (X)), the carrier of (X)))
the L_join of (X) . ((Y "/\" A1),A1) is Element of the carrier of (X)
(X) is non empty set
a9 is Element of (X)
f is Element of (X)
the L_meet of (X) . (a9,f) is set
the L_join of (X) . (( the L_meet of (X) . (a9,f)),f) is set
X is non empty with_tolerance L6()
(X) is non empty strict LattStr
the carrier of (X) is non empty set
Y is Element of the carrier of (X)
A1 is Element of the carrier of (X)
Y "/\" A1 is Element of the carrier of (X)
the L_meet of (X) is V1() V4(K20( the carrier of (X), the carrier of (X))) V5( the carrier of (X)) V6() V18(K20( the carrier of (X), the carrier of (X)), the carrier of (X)) Element of K19(K20(K20( the carrier of (X), the carrier of (X)), the carrier of (X)))
K20( the carrier of (X), the carrier of (X)) is non empty set
K20(K20( the carrier of (X), the carrier of (X)), the carrier of (X)) is non empty set
K19(K20(K20( the carrier of (X), the carrier of (X)), the carrier of (X))) is non empty set
the L_meet of (X) . (Y,A1) is Element of the carrier of (X)
A1 "/\" Y is Element of the carrier of (X)
the L_meet of (X) . (A1,Y) is Element of the carrier of (X)
(X) is non empty set
A2 is Element of (X)
a9 is Element of (X)
f is (X)
f is (X)
(X,f,f) is (X)
the carrier of X is non empty set
(X,f) is Element of K19( the carrier of X)
K19( the carrier of X) is non empty set
f `1 is set
(X,f) is Element of K19( the carrier of X)
f `1 is set
(X,f) /\ (X,f) is Element of K19( the carrier of X)
(X,f) is Element of K19( the carrier of X)
f `2 is set
(X,f) is Element of K19( the carrier of X)
f `2 is set
(X,f) /\ (X,f) is Element of K19( the carrier of X)
[((X,f) /\ (X,f)),((X,f) /\ (X,f))] is V15() set
{((X,f) /\ (X,f)),((X,f) /\ (X,f))} is non empty set
{((X,f) /\ (X,f))} is non empty set
{{((X,f) /\ (X,f)),((X,f) /\ (X,f))},{((X,f) /\ (X,f))}} is non empty set
(X,f,f) is (X)
(X,f) /\ (X,f) is Element of K19( the carrier of X)
(X,f) /\ (X,f) is Element of K19( the carrier of X)
[((X,f) /\ (X,f)),((X,f) /\ (X,f))] is V15() set
{((X,f) /\ (X,f)),((X,f) /\ (X,f))} is non empty set
{((X,f) /\ (X,f))} is non empty set
{{((X,f) /\ (X,f)),((X,f) /\ (X,f))},{((X,f) /\ (X,f))}} is non empty set
X is non empty with_tolerance L6()
(X) is non empty strict LattStr
the carrier of (X) is non empty set
Y is Element of the carrier of (X)
A1 is Element of the carrier of (X)
A2 is Element of the carrier of (X)
A1 "/\" A2 is Element of the carrier of (X)
the L_meet of (X) is V1() V4(K20( the carrier of (X), the carrier of (X))) V5( the carrier of (X)) V6() V18(K20( the carrier of (X), the carrier of (X)), the carrier of (X)) Element of K19(K20(K20( the carrier of (X), the carrier of (X)), the carrier of (X)))
K20( the carrier of (X), the carrier of (X)) is non empty set
K20(K20( the carrier of (X), the carrier of (X)), the carrier of (X)) is non empty set
K19(K20(K20( the carrier of (X), the carrier of (X)), the carrier of (X))) is non empty set
the L_meet of (X) . (A1,A2) is Element of the carrier of (X)
Y "/\" (A1 "/\" A2) is Element of the carrier of (X)
the L_meet of (X) . (Y,(A1 "/\" A2)) is Element of the carrier of (X)
Y "/\" A1 is Element of the carrier of (X)
the L_meet of (X) . (Y,A1) is Element of the carrier of (X)
(Y "/\" A1) "/\" A2 is Element of the carrier of (X)
the L_meet of (X) . ((Y "/\" A1),A2) is Element of the carrier of (X)
(X) is non empty set
a9 is Element of (X)
f is Element of (X)
f is Element of (X)
g is (X)
a9 is (X)
(X,g,a9) is (X)
the carrier of X is non empty set
(X,g) is Element of K19( the carrier of X)
K19( the carrier of X) is non empty set
g `1 is set
(X,a9) is Element of K19( the carrier of X)
a9 `1 is set
(X,g) /\ (X,a9) is Element of K19( the carrier of X)
(X,g) is Element of K19( the carrier of X)
g `2 is set
(X,a9) is Element of K19( the carrier of X)
a9 `2 is set
(X,g) /\ (X,a9) is Element of K19( the carrier of X)
[((X,g) /\ (X,a9)),((X,g) /\ (X,a9))] is V15() set
{((X,g) /\ (X,a9)),((X,g) /\ (X,a9))} is non empty set
{((X,g) /\ (X,a9))} is non empty set
{{((X,g) /\ (X,a9)),((X,g) /\ (X,a9))},{((X,g) /\ (X,a9))}} is non empty set
g is (X)
(X,g,g) is (X)
(X,g) is Element of K19( the carrier of X)
g `1 is set
(X,g) /\ (X,g) is Element of K19( the carrier of X)
(X,g) is Element of K19( the carrier of X)
g `2 is set
(X,g) /\ (X,g) is Element of K19( the carrier of X)
[((X,g) /\ (X,g)),((X,g) /\ (X,g))] is V15() set
{((X,g) /\ (X,g)),((X,g) /\ (X,g))} is non empty set
{((X,g) /\ (X,g))} is non empty set
{{((X,g) /\ (X,g)),((X,g) /\ (X,g))},{((X,g) /\ (X,g))}} is non empty set
the L_meet of (X) . (a9,(X,g,a9)) is set
(X,g,(X,g,a9)) is (X)
(X,(X,g,a9)) is Element of K19( the carrier of X)
(X,g,a9) `1 is set
(X,g) /\ (X,(X,g,a9)) is Element of K19( the carrier of X)
(X,(X,g,a9)) is Element of K19( the carrier of X)
(X,g,a9) `2 is set
(X,g) /\ (X,(X,g,a9)) is Element of K19( the carrier of X)
[((X,g) /\ (X,(X,g,a9))),((X,g) /\ (X,(X,g,a9)))] is V15() set
{((X,g) /\ (X,(X,g,a9))),((X,g) /\ (X,(X,g,a9)))} is non empty set
{((X,g) /\ (X,(X,g,a9)))} is non empty set
{{((X,g) /\ (X,(X,g,a9))),((X,g) /\ (X,(X,g,a9)))},{((X,g) /\ (X,(X,g,a9)))}} is non empty set
(X,(X,g,g),a9) is (X)
(X,(X,g,g)) is Element of K19( the carrier of X)
(X,g,g) `1 is set
(X,(X,g,g)) /\ (X,a9) is Element of K19( the carrier of X)
(X,(X,g,g)) is Element of K19( the carrier of X)
(X,g,g) `2 is set
(X,(X,g,g)) /\ (X,a9) is Element of K19( the carrier of X)
[((X,(X,g,g)) /\ (X,a9)),((X,(X,g,g)) /\ (X,a9))] is V15() set
{((X,(X,g,g)) /\ (X,a9)),((X,(X,g,g)) /\ (X,a9))} is non empty set
{((X,(X,g,g)) /\ (X,a9))} is non empty set
{{((X,(X,g,g)) /\ (X,a9)),((X,(X,g,g)) /\ (X,a9))},{((X,(X,g,g)) /\ (X,a9))}} is non empty set
the L_meet of (X) . ((X,g,g),f) is set
X is non empty with_tolerance L6()
(X) is non empty set
(X) is non empty strict LattStr
the L_meet of (X) is V1() V4(K20( the carrier of (X), the carrier of (X))) V5( the carrier of (X)) V6() V18(K20( the carrier of (X), the carrier of (X)), the carrier of (X)) Element of K19(K20(K20( the carrier of (X), the carrier of (X)), the carrier of (X)))
the carrier of (X) is non empty set
K20( the carrier of (X), the carrier of (X)) is non empty set
K20(K20( the carrier of (X), the carrier of (X)), the carrier of (X)) is non empty set
K19(K20(K20( the carrier of (X), the carrier of (X)), the carrier of (X))) is non empty set
the L_join of (X) is V1() V4(K20( the carrier of (X), the carrier of (X))) V5( the carrier of (X)) V6() V18(K20( the carrier of (X), the carrier of (X)), the carrier of (X)) Element of K19(K20(K20( the carrier of (X), the carrier of (X)), the carrier of (X)))
Y is Element of (X)
A1 is Element of (X)
the L_meet of (X) . (Y,A1) is set
A2 is Element of (X)
the L_join of (X) . (A1,A2) is set
the L_meet of (X) . (Y,( the L_join of (X) . (A1,A2))) is set
the L_meet of (X) . (Y,A2) is set
the L_join of (X) . (( the L_meet of (X) . (Y,A1)),( the L_meet of (X) . (Y,A2))) is set
f is (X)
g is (X)
(X,f,g) is (X)
the carrier of X is non empty set
(X,f) is Element of K19( the carrier of X)
K19( the carrier of X) is non empty set
f `1 is set
(X,g) is Element of K19( the carrier of X)
g `1 is set
(X,f) \/ (X,g) is Element of K19( the carrier of X)
(X,f) is Element of K19( the carrier of X)
f `2 is set
(X,g) is Element of K19( the carrier of X)
g `2 is set
(X,f) \/ (X,g) is Element of K19( the carrier of X)
[((X,f) \/ (X,g)),((X,f) \/ (X,g))] is V15() set
{((X,f) \/ (X,g)),((X,f) \/ (X,g))} is non empty set
{((X,f) \/ (X,g))} is non empty set
{{((X,f) \/ (X,g)),((X,f) \/ (X,g))},{((X,f) \/ (X,g))}} is non empty set
f is (X)
(X,f,f) is (X)
(X,f) is Element of K19( the carrier of X)
f `1 is set
(X,f) /\ (X,f) is Element of K19( the carrier of X)
(X,f) is Element of K19( the carrier of X)
f `2 is set
(X,f) /\ (X,f) is Element of K19( the carrier of X)
[((X,f) /\ (X,f)),((X,f) /\ (X,f))] is V15() set
{((X,f) /\ (X,f)),((X,f) /\ (X,f))} is non empty set
{((X,f) /\ (X,f))} is non empty set
{{((X,f) /\ (X,f)),((X,f) /\ (X,f))},{((X,f) /\ (X,f))}} is non empty set
(X,f,g) is (X)
(X,f) /\ (X,g) is Element of K19( the carrier of X)
(X,f) /\ (X,g) is Element of K19( the carrier of X)
[((X,f) /\ (X,g)),((X,f) /\ (X,g))] is V15() set
{((X,f) /\ (X,g)),((X,f) /\ (X,g))} is non empty set
{((X,f) /\ (X,g))} is non empty set
{{((X,f) /\ (X,g)),((X,f) /\ (X,g))},{((X,f) /\ (X,g))}} is non empty set
the L_meet of (X) . (Y,(X,f,g)) is set
(X,f,(X,f,g)) is (X)
(X,(X,f,g)) is Element of K19( the carrier of X)
(X,f,g) `1 is set
(X,f) /\ (X,(X,f,g)) is Element of K19( the carrier of X)
(X,(X,f,g)) is Element of K19( the carrier of X)
(X,f,g) `2 is set
(X,f) /\ (X,(X,f,g)) is Element of K19( the carrier of X)
[((X,f) /\ (X,(X,f,g))),((X,f) /\ (X,(X,f,g)))] is V15() set
{((X,f) /\ (X,(X,f,g))),((X,f) /\ (X,(X,f,g)))} is non empty set
{((X,f) /\ (X,(X,f,g)))} is non empty set
{{((X,f) /\ (X,(X,f,g))),((X,f) /\ (X,(X,f,g)))},{((X,f) /\ (X,(X,f,g)))}} is non empty set
(X,(X,f,f),(X,f,g)) is (X)
(X,(X,f,f)) is Element of K19( the carrier of X)
(X,f,f) `1 is set
(X,(X,f,g)) is Element of K19( the carrier of X)
(X,f,g) `1 is set
(X,(X,f,f)) \/ (X,(X,f,g)) is Element of K19( the carrier of X)
(X,(X,f,f)) is Element of K19( the carrier of X)
(X,f,f) `2 is set
(X,(X,f,g)) is Element of K19( the carrier of X)
(X,f,g) `2 is set
(X,(X,f,f)) \/ (X,(X,f,g)) is Element of K19( the carrier of X)
[((X,(X,f,f)) \/ (X,(X,f,g))),((X,(X,f,f)) \/ (X,(X,f,g)))] is V15() set
{((X,(X,f,f)) \/ (X,(X,f,g))),((X,(X,f,f)) \/ (X,(X,f,g)))} is non empty set
{((X,(X,f,f)) \/ (X,(X,f,g)))} is non empty set
{{((X,(X,f,f)) \/ (X,(X,f,g))),((X,(X,f,f)) \/ (X,(X,f,g)))},{((X,(X,f,f)) \/ (X,(X,f,g)))}} is non empty set
the L_join of (X) . ((X,f,f),(X,f,g)) is set
the L_join of (X) . (( the L_meet of (X) . (Y,A1)),(X,f,g)) is set
X is non empty with_tolerance L6()
(X) is non empty strict LattStr
the carrier of (X) is non empty set
Y is Element of the carrier of (X)
A1 is Element of the carrier of (X)
Y "\/" A1 is Element of the carrier of (X)
the L_join of (X) is V1() V4(K20( the carrier of (X), the carrier of (X))) V5( the carrier of (X)) V6() V18(K20( the carrier of (X), the carrier of (X)), the carrier of (X)) Element of K19(K20(K20( the carrier of (X), the carrier of (X)), the carrier of (X)))
K20( the carrier of (X), the carrier of (X)) is non empty set
K20(K20( the carrier of (X), the carrier of (X)), the carrier of (X)) is non empty set
K19(K20(K20( the carrier of (X), the carrier of (X)), the carrier of (X))) is non empty set
the L_join of (X) . (Y,A1) is Element of the carrier of (X)
Y "/\" (Y "\/" A1) is Element of the carrier of (X)
the L_meet of (X) is V1() V4(K20( the carrier of (X), the carrier of (X))) V5( the carrier of (X)) V6() V18(K20( the carrier of (X), the carrier of (X)), the carrier of (X)) Element of K19(K20(K20( the carrier of (X), the carrier of (X)), the carrier of (X)))
the L_meet of (X) . (Y,(Y "\/" A1)) is Element of the carrier of (X)
(X) is non empty set
a9 is Element of (X)
the L_meet of (X) . (a9,a9) is set
f is Element of (X)
the L_meet of (X) . (a9,f) is set
the L_join of (X) . (( the L_meet of (X) . (a9,a9)),( the L_meet of (X) . (a9,f))) is set
f is (X)
(X,f,f) is (X)
the carrier of X is non empty set
(X,f) is Element of K19( the carrier of X)
K19( the carrier of X) is non empty set
f `1 is set
(X,f) /\ (X,f) is Element of K19( the carrier of X)
(X,f) is Element of K19( the carrier of X)
f `2 is set
(X,f) /\ (X,f) is Element of K19( the carrier of X)
[((X,f) /\ (X,f)),((X,f) /\ (X,f))] is V15() set
{((X,f) /\ (X,f)),((X,f) /\ (X,f))} is non empty set
{((X,f) /\ (X,f))} is non empty set
{{((X,f) /\ (X,f)),((X,f) /\ (X,f))},{((X,f) /\ (X,f))}} is non empty set
the L_join of (X) . ((X,f,f),( the L_meet of (X) . (a9,f))) is set
Y "/\" A1 is Element of the carrier of (X)
the L_meet of (X) . (Y,A1) is Element of the carrier of (X)
Y "\/" (Y "/\" A1) is Element of the carrier of (X)
the L_join of (X) . (Y,(Y "/\" A1)) is Element of the carrier of (X)
(Y "/\" A1) "\/" Y is Element of the carrier of (X)
the L_join of (X) . ((Y "/\" A1),Y) is Element of the carrier of (X)
A1 "/\" Y is Element of the carrier of (X)
the L_meet of (X) . (A1,Y) is Element of the carrier of (X)
(A1 "/\" Y) "\/" Y is Element of the carrier of (X)
the L_join of (X) . ((A1 "/\" Y),Y) is Element of the carrier of (X)
X is non empty with_tolerance L6()
(X) is non empty strict LattStr
the carrier of (X) is non empty set
A1 is Element of the carrier of (X)
A2 is Element of the carrier of (X)
A1 "\/" A2 is Element of the carrier of (X)
the L_join of (X) is V1() V4(K20( the carrier of (X), the carrier of (X))) V5( the carrier of (X)) V6() V18(K20( the carrier of (X), the carrier of (X)), the carrier of (X)) Element of K19(K20(K20( the carrier of (X), the carrier of (X)), the carrier of (X)))
K20( the carrier of (X), the carrier of (X)) is non empty set
K20(K20( the carrier of (X), the carrier of (X)), the carrier of (X)) is non empty set
K19(K20(K20( the carrier of (X), the carrier of (X)), the carrier of (X))) is non empty set
the L_join of (X) . (A1,A2) is Element of the carrier of (X)
A2 "\/" A1 is Element of the carrier of (X)
the L_join of (X) . (A2,A1) is Element of the carrier of (X)
A1 is Element of the carrier of (X)
A2 is Element of the carrier of (X)
a9 is Element of the carrier of (X)
A2 "\/" a9 is Element of the carrier of (X)
the L_join of (X) is V1() V4(K20( the carrier of (X), the carrier of (X))) V5( the carrier of (X)) V6() V18(K20( the carrier of (X), the carrier of (X)), the carrier of (X)) Element of K19(K20(K20( the carrier of (X), the carrier of (X)), the carrier of (X)))
K20( the carrier of (X), the carrier of (X)) is non empty set
K20(K20( the carrier of (X), the carrier of (X)), the carrier of (X)) is non empty set
K19(K20(K20( the carrier of (X), the carrier of (X)), the carrier of (X))) is non empty set
the L_join of (X) . (A2,a9) is Element of the carrier of (X)
A1 "\/" (A2 "\/" a9) is Element of the carrier of (X)
the L_join of (X) . (A1,(A2 "\/" a9)) is Element of the carrier of (X)
A1 "\/" A2 is Element of the carrier of (X)
the L_join of (X) . (A1,A2) is Element of the carrier of (X)
(A1 "\/" A2) "\/" a9 is Element of the carrier of (X)
the L_join of (X) . ((A1 "\/" A2),a9) is Element of the carrier of (X)
A1 is Element of the carrier of (X)
A2 is Element of the carrier of (X)
A1 "/\" A2 is Element of the carrier of (X)
the L_meet of (X) is V1() V4(K20( the carrier of (X), the carrier of (X))) V5( the carrier of (X)) V6() V18(K20( the carrier of (X), the carrier of (X)), the carrier of (X)) Element of K19(K20(K20( the carrier of (X), the carrier of (X)), the carrier of (X)))
K20( the carrier of (X), the carrier of (X)) is non empty set
K20(K20( the carrier of (X), the carrier of (X)), the carrier of (X)) is non empty set
K19(K20(K20( the carrier of (X), the carrier of (X)), the carrier of (X))) is non empty set
the L_meet of (X) . (A1,A2) is Element of the carrier of (X)
(A1 "/\" A2) "\/" A2 is Element of the carrier of (X)
the L_join of (X) is V1() V4(K20( the carrier of (X), the carrier of (X))) V5( the carrier of (X)) V6() V18(K20( the carrier of (X), the carrier of (X)), the carrier of (X)) Element of K19(K20(K20( the carrier of (X), the carrier of (X)), the carrier of (X)))
the L_join of (X) . ((A1 "/\" A2),A2) is Element of the carrier of (X)
A1 is Element of the carrier of (X)
A2 is Element of the carrier of (X)
A1 "/\" A2 is Element of the carrier of (X)
the L_meet of (X) is V1() V4(K20( the carrier of (X), the carrier of (X))) V5( the carrier of (X)) V6() V18(K20( the carrier of (X), the carrier of (X)), the carrier of (X)) Element of K19(K20(K20( the carrier of (X), the carrier of (X)), the carrier of (X)))
K20( the carrier of (X), the carrier of (X)) is non empty set
K20(K20( the carrier of (X), the carrier of (X)), the carrier of (X)) is non empty set
K19(K20(K20( the carrier of (X), the carrier of (X)), the carrier of (X))) is non empty set
the L_meet of (X) . (A1,A2) is Element of the carrier of (X)
A2 "/\" A1 is Element of the carrier of (X)
the L_meet of (X) . (A2,A1) is Element of the carrier of (X)
A1 is Element of the carrier of (X)
A2 is Element of the carrier of (X)
a9 is Element of the carrier of (X)
A2 "/\" a9 is Element of the carrier of (X)
the L_meet of (X) is V1() V4(K20( the carrier of (X), the carrier of (X))) V5( the carrier of (X)) V6() V18(K20( the carrier of (X), the carrier of (X)), the carrier of (X)) Element of K19(K20(K20( the carrier of (X), the carrier of (X)), the carrier of (X)))
K20( the carrier of (X), the carrier of (X)) is non empty set
K20(K20( the carrier of (X), the carrier of (X)), the carrier of (X)) is non empty set
K19(K20(K20( the carrier of (X), the carrier of (X)), the carrier of (X))) is non empty set
the L_meet of (X) . (A2,a9) is Element of the carrier of (X)
A1 "/\" (A2 "/\" a9) is Element of the carrier of (X)
the L_meet of (X) . (A1,(A2 "/\" a9)) is Element of the carrier of (X)
A1 "/\" A2 is Element of the carrier of (X)
the L_meet of (X) . (A1,A2) is Element of the carrier of (X)
(A1 "/\" A2) "/\" a9 is Element of the carrier of (X)
the L_meet of (X) . ((A1 "/\" A2),a9) is Element of the carrier of (X)
A1 is Element of the carrier of (X)
A2 is Element of the carrier of (X)
A1 "\/" A2 is Element of the carrier of (X)
the L_join of (X) is V1() V4(K20( the carrier of (X), the carrier of (X))) V5( the carrier of (X)) V6() V18(K20( the carrier of (X), the carrier of (X)), the carrier of (X)) Element of K19(K20(K20( the carrier of (X), the carrier of (X)), the carrier of (X)))
K20( the carrier of (X), the carrier of (X)) is non empty set
K20(K20( the carrier of (X), the carrier of (X)), the carrier of (X)) is non empty set
K19(K20(K20( the carrier of (X), the carrier of (X)), the carrier of (X))) is non empty set
the L_join of (X) . (A1,A2) is Element of the carrier of (X)
A1 "/\" (A1 "\/" A2) is Element of the carrier of (X)
the L_meet of (X) is V1() V4(K20( the carrier of (X), the carrier of (X))) V5( the carrier of (X)) V6() V18(K20( the carrier of (X), the carrier of (X)), the carrier of (X)) Element of K19(K20(K20( the carrier of (X), the carrier of (X)), the carrier of (X)))
the L_meet of (X) . (A1,(A1 "\/" A2)) is Element of the carrier of (X)
X is non empty with_tolerance L6()
(X) is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like LattStr
the carrier of (X) is non empty set
Y is Element of the carrier of (X)
A1 is Element of the carrier of (X)
A2 is Element of the carrier of (X)
A1 "\/" A2 is Element of the carrier of (X)
the L_join of (X) is V1() V4(K20( the carrier of (X), the carrier of (X))) V5( the carrier of (X)) V6() V18(K20( the carrier of (X), the carrier of (X)), the carrier of (X)) Element of K19(K20(K20( the carrier of (X), the carrier of (X)), the carrier of (X)))
K20( the carrier of (X), the carrier of (X)) is non empty set
K20(K20( the carrier of (X), the carrier of (X)), the carrier of (X)) is non empty set
K19(K20(K20( the carrier of (X), the carrier of (X)), the carrier of (X))) is non empty set
the L_join of (X) . (A1,A2) is Element of the carrier of (X)
Y "/\" (A1 "\/" A2) is Element of the carrier of (X)
the L_meet of (X) is V1() V4(K20( the carrier of (X), the carrier of (X))) V5( the carrier of (X)) V6() V18(K20( the carrier of (X), the carrier of (X)), the carrier of (X)) Element of K19(K20(K20( the carrier of (X), the carrier of (X)), the carrier of (X)))
the L_meet of (X) . (Y,(A1 "\/" A2)) is Element of the carrier of (X)
Y "/\" A1 is Element of the carrier of (X)
the L_meet of (X) . (Y,A1) is Element of the carrier of (X)
Y "/\" A2 is Element of the carrier of (X)
the L_meet of (X) . (Y,A2) is Element of the carrier of (X)
(Y "/\" A1) "\/" (Y "/\" A2) is Element of the carrier of (X)
the L_join of (X) . ((Y "/\" A1),(Y "/\" A2)) is Element of the carrier of (X)
(X) is non empty set
A1 "\/" A2 is Element of the carrier of (X)
Y "/\" (A1 "\/" A2) is Element of the carrier of (X)
the L_meet of (X) . (Y,(A1 "\/" A2)) is Element of the carrier of (X)
a9 is Element of (X)
f is Element of (X)
the L_meet of (X) . (a9,f) is set
f is Element of (X)
the L_meet of (X) . (a9,f) is set
the L_join of (X) . (( the L_meet of (X) . (a9,f)),( the L_meet of (X) . (a9,f))) is set
Y "/\" A1 is Element of the carrier of (X)
Y "/\" A2 is Element of the carrier of (X)
(Y "/\" A1) "\/" (Y "/\" A2) is Element of the carrier of (X)
the L_join of (X) . ((Y "/\" A1),(Y "/\" A2)) is Element of the carrier of (X)
[{},{}] is V15() set
{{},{}} is non empty set
{{}} is non empty set
{{{},{}},{{}}} is non empty set
X is non empty with_tolerance L6()
the carrier of X is non empty set
K19( the carrier of X) is non empty set
Y is Element of K19( the carrier of X)
{} X is empty proper Element of K19( the carrier of X)
LAp Y is Element of K19( the carrier of X)
UAp Y is Element of K19( the carrier of X)
[(LAp Y),(UAp Y)] is V15() set
{(LAp Y),(UAp Y)} is non empty set
{(LAp Y)} is non empty set
{{(LAp Y),(UAp Y)},{(LAp Y)}} is non empty set
bool the carrier of X is non empty Element of K19(K19( the carrier of X))
K19(K19( the carrier of X)) is non empty set
[:(bool the carrier of X),(bool the carrier of X):] is V1() V4(K19( the carrier of X)) V5(K19( the carrier of X)) non empty Element of K19(K20(K19( the carrier of X),K19( the carrier of X)))
K20(K19( the carrier of X),K19( the carrier of X)) is non empty set
K19(K20(K19( the carrier of X),K19( the carrier of X))) is non empty set
X is non empty with_tolerance L6()
(X) is (X)
(X) is non empty set
X is non empty with_tolerance L6()
(X) is (X)
Y is (X)
(X,(X),Y) is (X)
the carrier of X is non empty set
(X,(X)) is Element of K19( the carrier of X)
K19( the carrier of X) is non empty set
(X) `1 is set
(X,Y) is Element of K19( the carrier of X)
Y `1 is set
(X,(X)) \/ (X,Y) is Element of K19( the carrier of X)
(X,(X)) is Element of K19( the carrier of X)
(X) `2 is set
(X,Y) is Element of K19( the carrier of X)
Y `2 is set
(X,(X)) \/ (X,Y) is Element of K19( the carrier of X)
[((X,(X)) \/ (X,Y)),((X,(X)) \/ (X,Y))] is V15() set
{((X,(X)) \/ (X,Y)),((X,(X)) \/ (X,Y))} is non empty set
{((X,(X)) \/ (X,Y))} is non empty set
{{((X,(X)) \/ (X,Y)),((X,(X)) \/ (X,Y))},{((X,(X)) \/ (X,Y))}} is non empty set
(X,(X,(X),Y)) is Element of K19( the carrier of X)
(X,(X),Y) `1 is set
(X,(X,(X),Y)) is Element of K19( the carrier of X)
(X,(X),Y) `2 is set
X is non empty with_tolerance L6()
[#] X is non empty non proper Element of K19( the carrier of X)
the carrier of X is non empty set
K19( the carrier of X) is non empty set
[([#] X),([#] X)] is V15() set
{([#] X),([#] X)} is non empty set
{([#] X)} is non empty set
{{([#] X),([#] X)},{([#] X)}} is non empty set
Y is Element of K19( the carrier of X)
LAp Y is Element of K19( the carrier of X)
UAp Y is Element of K19( the carrier of X)
[(LAp Y),(UAp Y)] is V15() set
{(LAp Y),(UAp Y)} is non empty set
{(LAp Y)} is non empty set
{{(LAp Y),(UAp Y)},{(LAp Y)}} is non empty set
bool the carrier of X is non empty Element of K19(K19( the carrier of X))
K19(K19( the carrier of X)) is non empty set
[:(bool the carrier of X),(bool the carrier of X):] is V1() V4(K19( the carrier of X)) V5(K19( the carrier of X)) non empty Element of K19(K20(K19( the carrier of X),K19( the carrier of X)))
K20(K19( the carrier of X),K19( the carrier of X)) is non empty set
K19(K20(K19( the carrier of X),K19( the carrier of X))) is non empty set
X is non empty with_tolerance L6()
(X) is (X)
[#] X is non empty non proper Element of K19( the carrier of X)
the carrier of X is non empty set
K19( the carrier of X) is non empty set
[([#] X),([#] X)] is V15() set
{([#] X),([#] X)} is non empty set
{([#] X)} is non empty set
{{([#] X),([#] X)},{([#] X)}} is non empty set
(X) is non empty set
X is non empty with_tolerance L6()
(X) is (X)
[#] X is non empty non proper Element of K19( the carrier of X)
the carrier of X is non empty set
K19( the carrier of X) is non empty set
[([#] X),([#] X)] is V15() set
{([#] X),([#] X)} is non empty set
{([#] X)} is non empty set
{{([#] X),([#] X)},{([#] X)}} is non empty set
Y is (X)
(X,(X),Y) is (X)
(X,(X)) is Element of K19( the carrier of X)
(X) `1 is set
(X,Y) is Element of K19( the carrier of X)
Y `1 is set
(X,(X)) /\ (X,Y) is Element of K19( the carrier of X)
(X,(X)) is Element of K19( the carrier of X)
(X) `2 is set
(X,Y) is Element of K19( the carrier of X)
Y `2 is set
(X,(X)) /\ (X,Y) is Element of K19( the carrier of X)
[((X,(X)) /\ (X,Y)),((X,(X)) /\ (X,Y))] is V15() set
{((X,(X)) /\ (X,Y)),((X,(X)) /\ (X,Y))} is non empty set
{((X,(X)) /\ (X,Y))} is non empty set
{{((X,(X)) /\ (X,Y)),((X,(X)) /\ (X,Y))},{((X,(X)) /\ (X,Y))}} is non empty set
(X,(X,(X),Y)) is Element of K19( the carrier of X)
(X,(X),Y) `1 is set
(X,(X,(X),Y)) is Element of K19( the carrier of X)
(X,(X),Y) `2 is set
X is non empty with_tolerance L6()
(X) is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular LattStr
(X) is non empty set
(X) is (X)
the carrier of (X) is non empty set
Y is Element of (X)
A1 is Element of the carrier of (X)
A2 is Element of the carrier of (X)
A1 "/\" A2 is Element of the carrier of (X)
the L_meet of (X) is V1() V4(K20( the carrier of (X), the carrier of (X))) V5( the carrier of (X)) V6() V18(K20( the carrier of (X), the carrier of (X)), the carrier of (X)) Element of K19(K20(K20( the carrier of (X), the carrier of (X)), the carrier of (X)))
K20( the carrier of (X), the carrier of (X)) is non empty set
K20(K20( the carrier of (X), the carrier of (X)), the carrier of (X)) is non empty set
K19(K20(K20( the carrier of (X), the carrier of (X)), the carrier of (X))) is non empty set
the L_meet of (X) . (A1,A2) is Element of the carrier of (X)
A2 "/\" A1 is Element of the carrier of (X)
the L_meet of (X) . (A2,A1) is Element of the carrier of (X)
a9 is Element of (X)
A1 "\/" A2 is Element of the carrier of (X)
the L_join of (X) is V1() V4(K20( the carrier of (X), the carrier of (X))) V5( the carrier of (X)) V6() V18(K20( the carrier of (X), the carrier of (X)), the carrier of (X)) Element of K19(K20(K20( the carrier of (X), the carrier of (X)), the carrier of (X)))
the L_join of (X) . (A1,A2) is Element of the carrier of (X)
f is (X)
f is (X)
(X,f,f) is (X)
the carrier of X is non empty set
(X,f) is Element of K19( the carrier of X)
K19( the carrier of X) is non empty set
f `1 is set
(X,f) is Element of K19( the carrier of X)
f `1 is set
(X,f) \/ (X,f) is Element of K19( the carrier of X)
(X,f) is Element of K19( the carrier of X)
f `2 is set
(X,f) is Element of K19( the carrier of X)
f `2 is set
(X,f) \/ (X,f) is Element of K19( the carrier of X)
[((X,f) \/ (X,f)),((X,f) \/ (X,f))] is V15() set
{((X,f) \/ (X,f)),((X,f) \/ (X,f))} is non empty set
{((X,f) \/ (X,f))} is non empty set
{{((X,f) \/ (X,f)),((X,f) \/ (X,f))},{((X,f) \/ (X,f))}} is non empty set
A1 "/\" A2 is Element of the carrier of (X)
A2 "/\" A1 is Element of the carrier of (X)
(X) is non empty set
(X) is (X)
[#] X is non empty non proper Element of K19( the carrier of X)
the carrier of X is non empty set
K19( the carrier of X) is non empty set
[([#] X),([#] X)] is V15() set
{([#] X),([#] X)} is non empty set
{([#] X)} is non empty set
{{([#] X),([#] X)},{([#] X)}} is non empty set
the carrier of (X) is non empty set
Y is Element of (X)
A1 is Element of the carrier of (X)
A2 is Element of the carrier of (X)
A1 "\/" A2 is Element of the carrier of (X)
the L_join of (X) is V1() V4(K20( the carrier of (X), the carrier of (X))) V5( the carrier of (X)) V6() V18(K20( the carrier of (X), the carrier of (X)), the carrier of (X)) Element of K19(K20(K20( the carrier of (X), the carrier of (X)), the carrier of (X)))
K20( the carrier of (X), the carrier of (X)) is non empty set
K20(K20( the carrier of (X), the carrier of (X)), the carrier of (X)) is non empty set
K19(K20(K20( the carrier of (X), the carrier of (X)), the carrier of (X))) is non empty set
the L_join of (X) . (A1,A2) is Element of the carrier of (X)
A2 "\/" A1 is Element of the carrier of (X)
the L_join of (X) . (A2,A1) is Element of the carrier of (X)
a9 is Element of (X)
A1 "/\" A2 is Element of the carrier of (X)
the L_meet of (X) is V1() V4(K20( the carrier of (X), the carrier of (X))) V5( the carrier of (X)) V6() V18(K20( the carrier of (X), the carrier of (X)), the carrier of (X)) Element of K19(K20(K20( the carrier of (X), the carrier of (X)), the carrier of (X)))
the L_meet of (X) . (A1,A2) is Element of the carrier of (X)
f is (X)
f is (X)
(X,f,f) is (X)
(X,f) is Element of K19( the carrier of X)
f `1 is set
(X,f) is Element of K19( the carrier of X)
f `1 is set
(X,f) /\ (X,f) is Element of K19( the carrier of X)
(X,f) is Element of K19( the carrier of X)
f `2 is set
(X,f) is Element of K19( the carrier of X)
f `2 is set
(X,f) /\ (X,f) is Element of K19( the carrier of X)
[((X,f) /\ (X,f)),((X,f) /\ (X,f))] is V15() set
{((X,f) /\ (X,f)),((X,f) /\ (X,f))} is non empty set
{((X,f) /\ (X,f))} is non empty set
{{((X,f) /\ (X,f)),((X,f) /\ (X,f))},{((X,f) /\ (X,f))}} is non empty set
A1 "\/" A2 is Element of the carrier of (X)
A2 "\/" A1 is Element of the carrier of (X)
X is non empty with_tolerance L6()
(X) is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded bounded LattStr
the carrier of (X) is non empty set
Y is Element of the carrier of (X)
A1 is Element of the carrier of (X)
A2 is (X)
a9 is (X)
(X,A2) is Element of K19( the carrier of X)
the carrier of X is non empty set
K19( the carrier of X) is non empty set
A2 `1 is set
(X,a9) is Element of K19( the carrier of X)
a9 `1 is set
(X,A2) is Element of K19( the carrier of X)
A2 `2 is set
(X,a9) is Element of K19( the carrier of X)
a9 `2 is set
(X) is non empty set
Y "\/" A1 is Element of the carrier of (X)
the L_join of (X) is V1() V4(K20( the carrier of (X), the carrier of (X))) V5( the carrier of (X)) V6() V18(K20( the carrier of (X), the carrier of (X)), the carrier of (X)) Element of K19(K20(K20( the carrier of (X), the carrier of (X)), the carrier of (X)))
K20( the carrier of (X), the carrier of (X)) is non empty set
K20(K20( the carrier of (X), the carrier of (X)), the carrier of (X)) is non empty set
K19(K20(K20( the carrier of (X), the carrier of (X)), the carrier of (X))) is non empty set
the L_join of (X) . (Y,A1) is Element of the carrier of (X)
(X,A2,a9) is (X)
(X,A2) \/ (X,a9) is Element of K19( the carrier of X)
(X,A2) \/ (X,a9) is Element of K19( the carrier of X)
[((X,A2) \/ (X,a9)),((X,A2) \/ (X,a9))] is V15() set
{((X,A2) \/ (X,a9)),((X,A2) \/ (X,a9))} is non empty set
{((X,A2) \/ (X,a9))} is non empty set
{{((X,A2) \/ (X,a9)),((X,A2) \/ (X,a9))},{((X,A2) \/ (X,a9))}} is non empty set
(X,A2) \/ (X,a9) is Element of K19( the carrier of X)
(X,A2) \/ (X,a9) is Element of K19( the carrier of X)
(X,A2,a9) is (X)
[((X,A2) \/ (X,a9)),((X,A2) \/ (X,a9))] is V15() set
{((X,A2) \/ (X,a9)),((X,A2) \/ (X,a9))} is non empty set
{((X,A2) \/ (X,a9))} is non empty set
{{((X,A2) \/ (X,a9)),((X,A2) \/ (X,a9))},{((X,A2) \/ (X,a9))}} is non empty set
(X,(X,A2,a9)) is Element of K19( the carrier of X)
(X,A2,a9) `1 is set
(X,(X,A2,a9)) is Element of K19( the carrier of X)
(X,A2,a9) `2 is set
f is Element of (X)
f is Element of (X)
g is (X)
g is (X)
(X,g,g) is (X)
(X,g) is Element of K19( the carrier of X)
g `1 is set
(X,g) is Element of K19( the carrier of X)
g `1 is set
(X,g) \/ (X,g) is Element of K19( the carrier of X)
(X,g) is Element of K19( the carrier of X)
g `2 is set
(X,g) is Element of K19( the carrier of X)
g `2 is set
(X,g) \/ (X,g) is Element of K19( the carrier of X)
[((X,g) \/ (X,g)),((X,g) \/ (X,g))] is V15() set
{((X,g) \/ (X,g)),((X,g) \/ (X,g))} is non empty set
{((X,g) \/ (X,g))} is non empty set
{{((X,g) \/ (X,g)),((X,g) \/ (X,g))},{((X,g) \/ (X,g))}} is non empty set
Y "\/" A1 is Element of the carrier of (X)
the L_join of (X) is V1() V4(K20( the carrier of (X), the carrier of (X))) V5( the carrier of (X)) V6() V18(K20( the carrier of (X), the carrier of (X)), the carrier of (X)) Element of K19(K20(K20( the carrier of (X), the carrier of (X)), the carrier of (X)))
K20( the carrier of (X), the carrier of (X)) is non empty set
K20(K20( the carrier of (X), the carrier of (X)), the carrier of (X)) is non empty set
K19(K20(K20( the carrier of (X), the carrier of (X)), the carrier of (X))) is non empty set
the L_join of (X) . (Y,A1) is Element of the carrier of (X)
X is non empty with_tolerance L6()
(X) is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded bounded LattStr
the carrier of (X) is non empty set
K19( the carrier of (X)) is non empty set
Y is Element of K19( the carrier of (X))
Top (X) is Element of the carrier of (X)
A1 is Element of the carrier of (X)
A2 is Element of the carrier of (X)
A2 is Element of the carrier of (X)
{ (X,b<sub>1</sub>) where b<sub>1</sub> is (X) : b<sub>1</sub> in Y } is set
{ (X,b<sub>1</sub>) where b<sub>1</sub> is (X) : b<sub>1</sub> in Y } is set
meet { (X,b<sub>1</sub>) where b<sub>1</sub> is (X) : b<sub>1</sub> in Y } is set
meet { (X,b<sub>1</sub>) where b<sub>1</sub> is (X) : b<sub>1</sub> in Y } is set
[(meet { (X,b<sub>1</sub>) where b<sub>1</sub> is (X) : b<sub>1</sub> in Y } ),(meet { (X,b<sub>1</sub>) where b<sub>1</sub> is (X) : b<sub>1</sub> in Y } )] is V15() set
{(meet { (X,b<sub>1</sub>) where b<sub>1</sub> is (X) : b<sub>1</sub> in Y } ),(meet { (X,b<sub>1</sub>) where b<sub>1</sub> is (X) : b<sub>1</sub> in Y } )} is non empty set
{(meet { (X,b<sub>1</sub>) where b<sub>1</sub> is (X) : b<sub>1</sub> in Y } )} is non empty set
{{(meet { (X,b<sub>1</sub>) where b<sub>1</sub> is (X) : b<sub>1</sub> in Y } ),(meet { (X,b<sub>1</sub>) where b<sub>1</sub> is (X) : b<sub>1</sub> in Y } )},{(meet { (X,b<sub>1</sub>) where b<sub>1</sub> is (X) : b<sub>1</sub> in Y } )}} is non empty set
f is set
(X) is non empty set
K19((X)) is non empty set
f is (X)
(X,f) is Element of K19( the carrier of X)
the carrier of X is non empty set
K19( the carrier of X) is non empty set
f `1 is set
g is set
g is (X)
(X,g) is Element of K19( the carrier of X)
g `2 is set
a9 is set
a is set
a is set
b is (X)
(X,b) is Element of K19( the carrier of X)
b `1 is set
bool the carrier of X is non empty Element of K19(K19( the carrier of X))
K19(K19( the carrier of X)) is non empty set
a9 is set
a is set
a is set
b is (X)
(X,b) is Element of K19( the carrier of X)
b `2 is set
bool the carrier of X is non empty Element of K19(K19( the carrier of X))
K19(K19( the carrier of X)) is non empty set
[:(bool the carrier of X),(bool the carrier of X):] is V1() V4(K19( the carrier of X)) V5(K19( the carrier of X)) non empty Element of K19(K20(K19( the carrier of X),K19( the carrier of X)))
K20(K19( the carrier of X),K19( the carrier of X)) is non empty set
K19(K20(K19( the carrier of X),K19( the carrier of X))) is non empty set
a9 is (X)
a is Element of the carrier of (X)
b is Element of the carrier of (X)
b9 is (X)
a9 is Element of K19( the carrier of X)
Z1 is Element of K19( the carrier of X)
[a9,Z1] is V15() set
{a9,Z1} is non empty set
{a9} is non empty set
{{a9,Z1},{a9}} is non empty set
(X,b9) is Element of K19( the carrier of X)
b9 `1 is set
c2 is set
(X,a9) is Element of K19( the carrier of X)
a9 `1 is set
(X,a9) is Element of K19( the carrier of X)
a9 `2 is set
(X,b9) is Element of K19( the carrier of X)
b9 `2 is set
c2 is set
b is Element of the carrier of (X)
Z1 is Element of the carrier of (X)
b9 is (X)
(X,b9) is Element of K19( the carrier of X)
b9 `1 is set
Z1 is set
c2 is (X)
(X,c2) is Element of K19( the carrier of X)
c2 `1 is set
c29 is Element of the carrier of (X)
a9 is (X)
(X,a9) is Element of K19( the carrier of X)
a9 `1 is set
(X,b9) is Element of K19( the carrier of X)
b9 `2 is set
Z1 is set
c2 is (X)
(X,c2) is Element of K19( the carrier of X)
c2 `2 is set
c29 is Element of the carrier of (X)
(X,a9) is Element of K19( the carrier of X)
a9 `2 is set
A1 is Element of the carrier of (X)
X is non empty with_tolerance L6()
(X) is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded bounded LattStr