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

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

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

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

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

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

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

A2 is Element of K19(X)

a9 is Element of K19(X)

(X,A2,a9) is Element of K19(K19(X))

{ b

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

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

{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

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

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

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

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

a9 is Element of K19(X)

f is Element of K19(X)

(X,a9,f) is (X)

{ b

A1 is Element of K19(X)

A2 is Element of K19(X)

(X,A1,A2) is (X)

{ b

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

(X,A2,a9) is (X)

{ b

INTERSECTION ((X,Y,A1),(X,A2,a9)) is set

Y /\ A2 is Element of K19(X)

A1 /\ a9 is Element of K19(X)

{ b

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

(X,A2,a9) is (X)

{ b

UNION ((X,Y,A1),(X,A2,a9)) is set

Y \/ A2 is Element of K19(X)

A1 \/ a9 is Element of K19(X)

{ b

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

f is Element of K19(X)

g is Element of K19(X)

(X,f,g) is (X)

{ b

a9 /\ f is Element of K19(X)

f /\ g is Element of K19(X)

(X,(a9 /\ f),(f /\ g)) is (X)

{ b

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

f is Element of K19(X)

g is Element of K19(X)

(X,f,g) is (X)

{ b

a9 \/ f is Element of K19(X)

f \/ g is Element of K19(X)

(X,(a9 \/ f),(f \/ g)) is (X)

{ b

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

A1 is Element of K19(X)

a9 is Element of K19(X)

(X,A1,a9) is (X)

{ b

A2 is Element of K19(X)

f is Element of K19(X)

(X,A2,f) is (X)

{ b

A1 is Element of K19(X)

A2 is Element of K19(X)

(X,A1,A2) is (X)

{ b

a9 is Element of K19(X)

A1 is Element of K19(X)

(X,a9,A1) is (X)

{ b

f is Element of K19(X)

A2 is Element of K19(X)

(X,f,A2) is (X)

{ b

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

A2 is Element of K19(X)

(X,A2,(X,Y)) is (X)

{ b

(X,(X,Y),(X,Y)) is (X)

{ b

A2 is Element of K19(X)

(X,(X,Y),A2) is (X)

{ b

a9 is Element of K19(X)

(X,a9,(X,Y)) is (X)

{ b

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

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

A2 is Element of K19(X)

(X,A2,(X,Y)) is (X)

{ b

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

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

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

f is Element of K19(X)

(X,(X,Y),f) is (X)

{ b

g is Element of K19(X)

(X,(X,A1),g) is (X)

{ b

g is Element of K19(X)

(X,g,(X,Y)) is (X)

{ b

a9 is Element of K19(X)

(X,a9,(X,A1)) is (X)

{ b

A2 is set

a9 is Element of K19(X)

f is Element of K19(X)

(X,a9,f) is (X)

{ b

f is Element of K19(X)

(X,(X,A1),f) is (X)

{ b

g is Element of K19(X)

(X,(X,Y),g) is (X)

{ b

g is Element of K19(X)

(X,g,(X,A1)) is (X)

{ b

a9 is Element of K19(X)

(X,a9,(X,Y)) is (X)

{ b

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

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

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

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

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

(X,A2,a9) is (X)

{ b

DIFFERENCE ((X,Y,A1),(X,A2,a9)) is set

Y \ a9 is Element of K19(X)

A1 \ A2 is Element of K19(X)

{ b

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

f is Element of K19(X)

g is Element of K19(X)

(X,f,g) is (X)

{ b

a9 \ g is Element of K19(X)

f \ f is Element of K19(X)

(X,(a9 \ g),(f \ f)) is (X)

{ b

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

f is Element of K19(X)

f is Element of K19(X)

(X,f,f) is (X)

{ b

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

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

a9 is non empty (X) Element of K19(K19(X))

(X,(X,A1),(X,A1)) is (X)

{ b

(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

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

(X,Y) is Element of K19(X)

(X,Y) is Element of K19(X)

(X,(X,Y),(X,Y)) is (X)

{ b

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

f is Element of K19(X)

f is Element of K19(X)

(X,f,f) is (X)

{ b

A2 \ f is Element of K19(X)

a9 \ f is Element of K19(X)

(X,(A2 \ f),(a9 \ f)) is (X)

{ b

(X,Y) is Element of K19(X)

(X,Y) is Element of K19(X)

(X,(X,Y),(X,Y)) is (X)

{ b

(X,A1) is Element of K19(X)

(X,A1) is Element of K19(X)

(X,(X,A1),(X,A1)) is (X)

{ b

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

{([#] 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

{{}} 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

{} X is empty proper Element of K19(X)

(X,({} X),({} X)) is (X)

{ b

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

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

(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

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

(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

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

(X,Y) is Element of K19(X)

(X,Y) is Element of K19(X)

(X,(X,Y),(X,Y)) is (X)

{ b

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

(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

(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

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

(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

([#] X) ` is Element of K19(X)

X \ ([#] X) is set

(X,(([#] X) `),(([#] X) `)) is (X)

{ b

(X,({} X),(([#] X) `)) is (X)

{ b

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

[#] X is non empty non proper Element of K19(X)

(X,({} X),([#] X)) is (X)

{ b

Y is non empty (X)

(X,Y) is non empty (X)

(X,([#] X),([#] X)) is non empty (X)

{ b

(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

(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

(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

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

{} X is empty proper Element of K19(X)

(X,({} X),([#] X)) is (X)

{ b

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

(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

(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

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

[#] X is non empty non proper Element of K19(X)

(X,({} X),([#] X)) is (X)

{ b

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

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

(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

(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

(X,Y) \/ ((X,Y) `) is Element of K19(X)

(X,((X,Y) \/ ((X,Y) `)),((X,Y) \/ ((X,Y) `))) is (X)

{ b

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

(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

(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

(X,Y) /\ ((X,Y) `) is Element of K19(X)

(X,((X,Y) /\ ((X,Y) `)),((X,Y) /\ ((X,Y) `))) is (X)

{ b

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

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))},{