:: PZFMISC1 semantic presentation

{} is empty finite V29() set

dom {} is set

rng {} is set

I is set

A is set

B is set

A .--> B is Relation-like {A} -defined Function-like one-to-one finite set

{A} is non empty finite set

{A} --> B is Relation-like {A} -defined Function-like constant non empty V14({A}) V18({A},{B}) finite M2( bool [:{A},{B}:])

{B} is non empty finite set

[:{A},{B}:] is finite set

bool [:{A},{B}:] is finite V29() set

B is Relation-like I -defined Function-like V14(I) set

B +* (A .--> B) is Relation-like Function-like set

dom (B +* (A .--> B)) is set

dom B is set

dom (A .--> B) is finite set

(dom B) \/ (dom (A .--> B)) is set

I \/ (dom (A .--> B)) is set

I \/ {A} is non empty set

I is Relation-like Function-like set

I is set

A is Relation-like I -defined Function-like V14(I) set

B is set

A . B is set

I is set

A is Relation-like I -defined Function-like V14(I) set

B is Relation-like I -defined Function-like V14(I) set

B is Relation-like I -defined Function-like V14(I) set

y is set

B . y is set

A . y is set

{(A . y)} is non empty finite set

B . y is set

I is set

A is Relation-like I -defined Function-like V14(I) set

(I,A) is Relation-like I -defined Function-like V14(I) set

B is set

(I,A) . B is set

A . B is set

{(A . B)} is non empty finite set

B is set

(I,A) . B is set

A . B is set

{(A . B)} is non empty finite set

I is set

A is Relation-like I -defined Function-like V14(I) set

B is Relation-like I -defined Function-like V14(I) set

B is Relation-like I -defined Function-like V14(I) set

y is Relation-like I -defined Function-like V14(I) set

X is set

B . X is set

A . X is set

B . X is set

{(A . X),(B . X)} is non empty finite set

y . X is set

B is Relation-like I -defined Function-like V14(I) set

y is Relation-like I -defined Function-like V14(I) set

X is Relation-like I -defined Function-like V14(I) set

Y is set

B . Y is set

X . Y is set

y . Y is set

{(X . Y),(y . Y)} is non empty finite set

I is set

A is Relation-like I -defined Function-like V14(I) set

B is Relation-like I -defined Function-like V14(I) set

(I,A,B) is Relation-like I -defined Function-like V14(I) set

B is set

(I,A,B) . B is set

A . B is set

B . B is set

{(A . B),(B . B)} is non empty finite set

B is set

(I,A,B) . B is set

A . B is set

B . B is set

{(A . B),(B . B)} is non empty finite set

I is set

A is Relation-like I -defined Function-like V14(I) set

B is Relation-like I -defined Function-like V14(I) set

(I,B) is Relation-like non-empty I -defined Function-like V14(I) finite-yielding set

B is Relation-like I -defined Function-like V14(I) set

y is set

B . y is set

A . y is set

B . y is set

{(B . y)} is non empty finite set

y is set

B . y is set

A . y is set

B . y is set

{(B . y)} is non empty finite set

B is set

y is set

A . B is set

B . B is set

B .--> y is Relation-like {B} -defined Function-like one-to-one finite set

{B} is non empty finite set

{B} --> y is Relation-like {B} -defined Function-like constant non empty V14({B}) V18({B},{y}) finite M2( bool [:{B},{y}:])

{y} is non empty finite set

[:{B},{y}:] is finite set

bool [:{B},{y}:] is finite V29() set

dom (B .--> y) is finite set

B +* (B .--> y) is Relation-like Function-like set

dom (B +* (B .--> y)) is set

X is Relation-like I -defined Function-like V14(I) set

X . B is set

(B .--> y) . B is set

Y is set

X . Y is set

A . Y is set

B . Y is set

{(B . B)} is non empty finite set

(I,B) . B is finite set

I is set

A is Relation-like I -defined Function-like V14(I) set

B is Relation-like I -defined Function-like V14(I) set

B is Relation-like I -defined Function-like V14(I) set

(I,B,B) is Relation-like non-empty I -defined Function-like V14(I) finite-yielding set

y is set

X is set

A . y is set

B . y is set

B . y is set

y .--> X is Relation-like {y} -defined Function-like one-to-one finite set

{y} is non empty finite set

{y} --> X is Relation-like {y} -defined Function-like constant non empty V14({y}) V18({y},{X}) finite M2( bool [:{y},{X}:])

{X} is non empty finite set

[:{y},{X}:] is finite set

bool [:{y},{X}:] is finite V29() set

dom (y .--> X) is finite set

B +* (y .--> X) is Relation-like Function-like set

dom (B +* (y .--> X)) is set

Y is Relation-like I -defined Function-like V14(I) set

Y . y is set

(y .--> X) . y is set

i is set

Y . i is set

A . i is set

B . i is set

{(B . y),(B . y)} is non empty finite set

(I,B,B) . y is finite set

I is set

A is Relation-like I -defined Function-like V14(I) set

B is Relation-like I -defined Function-like V14(I) set

B is Relation-like I -defined Function-like V14(I) set

(I,B,B) is Relation-like non-empty I -defined Function-like V14(I) finite-yielding set

y is Relation-like I -defined Function-like V14(I) set

X is set

y . X is set

A . X is set

B . X is set

B . X is set

{(B . X),(B . X)} is non empty finite set

I is set

A is Relation-like I -defined Function-like V14(I) set

B is Relation-like I -defined Function-like V14(I) set

(I,B) is Relation-like non-empty I -defined Function-like V14(I) finite-yielding set

B is set

A . B is set

(I,B) . B is finite set

B . B is set

{(B . B)} is non empty finite set

I is set

A is Relation-like I -defined Function-like V14(I) set

(I,A) is Relation-like non-empty I -defined Function-like V14(I) finite-yielding set

B is set

A . B is set

(I,A) . B is finite set

{(A . B)} is non empty finite set

I is set

A is Relation-like I -defined Function-like V14(I) set

B is Relation-like I -defined Function-like V14(I) set

B is Relation-like I -defined Function-like V14(I) set

(I,B,B) is Relation-like non-empty I -defined Function-like V14(I) finite-yielding set

y is set

A . y is set

(I,B,B) . y is finite set

B . y is set

B . y is set

{(B . y),(B . y)} is non empty finite set

y is set

A . y is set

(I,B,B) . y is finite set

B . y is set

B . y is set

{(B . y),(B . y)} is non empty finite set

I is set

A is Relation-like I -defined Function-like V14(I) set

(I,A) is Relation-like non-empty I -defined Function-like V14(I) finite-yielding set

B is Relation-like I -defined Function-like V14(I) set

(I,B) is Relation-like non-empty I -defined Function-like V14(I) finite-yielding set

(I,A) \/ (I,B) is Relation-like I -defined Function-like V14(I) set

(I,A,B) is Relation-like non-empty I -defined Function-like V14(I) finite-yielding set

B is set

((I,A) \/ (I,B)) . B is set

(I,A) . B is finite set

(I,B) . B is finite set

((I,A) . B) \/ ((I,B) . B) is finite set

B . B is set

{(B . B)} is non empty finite set

((I,A) . B) \/ {(B . B)} is non empty finite set

A . B is set

{(A . B)} is non empty finite set

{(A . B)} \/ {(B . B)} is non empty finite set

{(A . B),(B . B)} is non empty finite set

(I,A,B) . B is finite set

I is set

A is Relation-like I -defined Function-like V14(I) set

(I,A,A) is Relation-like non-empty I -defined Function-like V14(I) finite-yielding set

(I,A) is Relation-like non-empty I -defined Function-like V14(I) finite-yielding set

B is set

(I,A,A) . B is finite set

A . B is set

{(A . B),(A . B)} is non empty finite set

{(A . B)} is non empty finite set

(I,A) . B is finite set

I is set

A is Relation-like I -defined Function-like V14(I) set

(I,A) is Relation-like non-empty I -defined Function-like V14(I) finite-yielding set

B is Relation-like I -defined Function-like V14(I) set

(I,B) is Relation-like non-empty I -defined Function-like V14(I) finite-yielding set

B is set

(I,A) . B is finite set

(I,B) . B is finite set

B . B is set

{(B . B)} is non empty finite set

A . B is set

{(A . B)} is non empty finite set

I is set

A is Relation-like I -defined Function-like V14(I) set

(I,A) is Relation-like non-empty I -defined Function-like V14(I) finite-yielding set

B is Relation-like I -defined Function-like V14(I) set

(I,B) is Relation-like non-empty I -defined Function-like V14(I) finite-yielding set

B is set

A . B is set

{(A . B)} is non empty finite set

(I,A) . B is finite set

B . B is set

{(B . B)} is non empty finite set

I is set

A is Relation-like I -defined Function-like V14(I) set

(I,A) is Relation-like non-empty I -defined Function-like V14(I) finite-yielding set

B is Relation-like I -defined Function-like V14(I) set

B is Relation-like I -defined Function-like V14(I) set

(I,B,B) is Relation-like non-empty I -defined Function-like V14(I) finite-yielding set

y is set

A . y is set

{(A . y)} is non empty finite set

(I,A) . y is finite set

B . y is set

B . y is set

{(B . y),(B . y)} is non empty finite set

y is set

A . y is set

{(A . y)} is non empty finite set

(I,A) . y is finite set

B . y is set

B . y is set

{(B . y),(B . y)} is non empty finite set

I is set

A is Relation-like I -defined Function-like V14(I) set

(I,A) is Relation-like non-empty I -defined Function-like V14(I) finite-yielding set

B is Relation-like I -defined Function-like V14(I) set

B is Relation-like I -defined Function-like V14(I) set

(I,B,B) is Relation-like non-empty I -defined Function-like V14(I) finite-yielding set

y is set

A . y is set

{(A . y)} is non empty finite set

(I,A) . y is finite set

B . y is set

B . y is set

{(B . y),(B . y)} is non empty finite set

I is set

A is Relation-like I -defined Function-like V14(I) set

(I,A) is Relation-like non-empty I -defined Function-like V14(I) finite-yielding set

B is Relation-like I -defined Function-like V14(I) set

(I,A,B) is Relation-like non-empty I -defined Function-like V14(I) finite-yielding set

(I,B) is Relation-like non-empty I -defined Function-like V14(I) finite-yielding set

B is set

(I,A) . B is finite set

(I,A,B) . B is finite set

A . B is set

{(A . B)} is non empty finite set

B . B is set

{(A . B),(B . B)} is non empty finite set

B is set

(I,B) . B is finite set

(I,A,B) . B is finite set

B . B is set

{(B . B)} is non empty finite set

A . B is set

{(A . B),(B . B)} is non empty finite set

I is set

A is Relation-like I -defined Function-like V14(I) set

(I,A) is Relation-like non-empty I -defined Function-like V14(I) finite-yielding set

B is Relation-like I -defined Function-like V14(I) set

(I,B) is Relation-like non-empty I -defined Function-like V14(I) finite-yielding set

(I,A) \/ (I,B) is Relation-like I -defined Function-like V14(I) set

B is set

A . B is set

{(A . B)} is non empty finite set

B . B is set

{(B . B)} is non empty finite set

{(A . B)} \/ {(B . B)} is non empty finite set

(I,B) . B is finite set

{(A . B)} \/ ((I,B) . B) is non empty finite set

(I,A) . B is finite set

((I,A) . B) \/ ((I,B) . B) is finite set

((I,A) \/ (I,B)) . B is set

A . B is set

{(A . B)} is non empty finite set

B . B is set

{(B . B)} is non empty finite set

{(A . B)} \/ {(B . B)} is non empty finite set

(I,B) . B is finite set

{(A . B)} \/ ((I,B) . B) is non empty finite set

(I,A) . B is finite set

((I,A) . B) \/ ((I,B) . B) is finite set

((I,A) \/ (I,B)) . B is set

I is set

A is Relation-like I -defined Function-like V14(I) set

(I,A) is Relation-like non-empty I -defined Function-like V14(I) finite-yielding set

B is Relation-like I -defined Function-like V14(I) set

(I,A,B) is Relation-like non-empty I -defined Function-like V14(I) finite-yielding set

(I,A) \/ (I,A,B) is Relation-like I -defined Function-like V14(I) set

B is set

((I,A) \/ (I,A,B)) . B is set

(I,A) . B is finite set

(I,A,B) . B is finite set

((I,A) . B) \/ ((I,A,B) . B) is finite set

A . B is set

{(A . B)} is non empty finite set

{(A . B)} \/ ((I,A,B) . B) is non empty finite set

B . B is set

{(A . B),(B . B)} is non empty finite set

{(A . B)} \/ {(A . B),(B . B)} is non empty finite set

I is set

[[0]] I is Relation-like I -defined Function-like V14(I) set

I --> {} is Relation-like I -defined Function-like constant V14(I) V18(I,{{}}) M2( bool [:I,{{}}:])

{{}} is non empty finite V29() set

[:I,{{}}:] is set

bool [:I,{{}}:] is set

A is Relation-like I -defined Function-like V14(I) set

(I,A) is Relation-like non-empty I -defined Function-like V14(I) finite-yielding set

B is Relation-like I -defined Function-like V14(I) set

(I,B) is Relation-like non-empty I -defined Function-like V14(I) finite-yielding set

(I,A) /\ (I,B) is Relation-like I -defined Function-like V14(I) set

B is set

y is set

A . y is set

{(A . y)} is non empty finite set

B . y is set

{(B . y)} is non empty finite set

{(A . y)} /\ {(B . y)} is finite set

(I,A) . y is finite set

((I,A) . y) /\ {(B . y)} is finite set

(I,B) . y is finite set

((I,A) . y) /\ ((I,B) . y) is finite set

((I,A) /\ (I,B)) . y is set

B is set

A . B is set

B . B is set

I is set

A is Relation-like I -defined Function-like V14(I) set

(I,A) is Relation-like non-empty I -defined Function-like V14(I) finite-yielding set

B is Relation-like I -defined Function-like V14(I) set

(I,B) is Relation-like non-empty I -defined Function-like V14(I) finite-yielding set

(I,A) /\ (I,B) is Relation-like I -defined Function-like V14(I) set

B is set

A . B is set

{(A . B)} is non empty finite set

B . B is set

{(B . B)} is non empty finite set

{(A . B)} /\ {(B . B)} is finite set

(I,B) . B is finite set

{(A . B)} /\ ((I,B) . B) is finite set

(I,A) . B is finite set

((I,A) . B) /\ ((I,B) . B) is finite set

((I,A) /\ (I,B)) . B is set

B is set

A . B is set

{(A . B)} is non empty finite set

B . B is set

{(B . B)} is non empty finite set

{(A . B)} /\ {(B . B)} is finite set

(I,B) . B is finite set

{(A . B)} /\ ((I,B) . B) is finite set

(I,A) . B is finite set

((I,A) . B) /\ ((I,B) . B) is finite set

((I,A) /\ (I,B)) . B is set

I is set

A is Relation-like I -defined Function-like V14(I) set

(I,A) is Relation-like non-empty I -defined Function-like V14(I) finite-yielding set

B is Relation-like I -defined Function-like V14(I) set

(I,A,B) is Relation-like non-empty I -defined Function-like V14(I) finite-yielding set

(I,A) /\ (I,A,B) is Relation-like I -defined Function-like V14(I) set

(I,B) is Relation-like non-empty I -defined Function-like V14(I) finite-yielding set

(I,B) /\ (I,A,B) is Relation-like I -defined Function-like V14(I) set

B is set

((I,A) /\ (I,A,B)) . B is set

(I,A) . B is finite set

(I,A,B) . B is finite set

((I,A) . B) /\ ((I,A,B) . B) is finite set

A . B is set

{(A . B)} is non empty finite set

{(A . B)} /\ ((I,A,B) . B) is finite set

B . B is set

{(A . B),(B . B)} is non empty finite set

{(A . B)} /\ {(A . B),(B . B)} is finite set

B is set

((I,B) /\ (I,A,B)) . B is set

(I,B) . B is finite set

(I,A,B) . B is finite set

((I,B) . B) /\ ((I,A,B) . B) is finite set

B . B is set

{(B . B)} is non empty finite set

{(B . B)} /\ ((I,A,B) . B) is finite set

A . B is set

{(A . B),(B . B)} is non empty finite set

{(B . B)} /\ {(A . B),(B . B)} is finite set

I is set

A is Relation-like I -defined Function-like V14(I) set

(I,A) is Relation-like non-empty I -defined Function-like V14(I) finite-yielding set

B is Relation-like I -defined Function-like V14(I) set

(I,B) is Relation-like non-empty I -defined Function-like V14(I) finite-yielding set

(I,A) \ (I,B) is Relation-like I -defined Function-like V14(I) set

B is set

y is set

A . y is set

{(A . y)} is non empty finite set

B . y is set

{(B . y)} is non empty finite set

{(A . y)} \ {(B . y)} is finite set

(I,A) . y is finite set

((I,A) . y) \ {(B . y)} is finite set

(I,B) . y is finite set

((I,A) . y) \ ((I,B) . y) is finite set

((I,A) \ (I,B)) . y is set

B is set

A . B is set

B . B is set

I is set

[[0]] I is Relation-like I -defined Function-like V14(I) set

I --> {} is Relation-like I -defined Function-like constant V14(I) V18(I,{{}}) M2( bool [:I,{{}}:])

{{}} is non empty finite V29() set

[:I,{{}}:] is set

bool [:I,{{}}:] is set

A is Relation-like I -defined Function-like V14(I) set

(I,A) is Relation-like non-empty I -defined Function-like V14(I) finite-yielding set

B is Relation-like I -defined Function-like V14(I) set

(I,B) is Relation-like non-empty I -defined Function-like V14(I) finite-yielding set

(I,A) \ (I,B) is Relation-like I -defined Function-like V14(I) set

B is set

A . B is set

{(A . B)} is non empty finite set

B . B is set

{(B . B)} is non empty finite set

{(A . B)} \ {(B . B)} is finite set

(I,A) . B is finite set

((I,A) . B) \ {(B . B)} is finite set

(I,B) . B is finite set

((I,A) . B) \ ((I,B) . B) is finite set

((I,A) \ (I,B)) . B is set

I is set

[[0]] I is Relation-like I -defined Function-like V14(I) set

I --> {} is Relation-like I -defined Function-like constant V14(I) V18(I,{{}}) M2( bool [:I,{{}}:])

{{}} is non empty finite V29() set

[:I,{{}}:] is set

bool [:I,{{}}:] is set

A is Relation-like I -defined Function-like V14(I) set

(I,A) is Relation-like non-empty I -defined Function-like V14(I) finite-yielding set

B is Relation-like I -defined Function-like V14(I) set

(I,A,B) is Relation-like non-empty I -defined Function-like V14(I) finite-yielding set

(I,A) \ (I,A,B) is Relation-like I -defined Function-like V14(I) set

(I,B) is Relation-like non-empty I -defined Function-like V14(I) finite-yielding set

(I,B) \ (I,A,B) is Relation-like I -defined Function-like V14(I) set

B is set

((I,A) \ (I,A,B)) . B is set

(I,A) . B is finite set

(I,A,B) . B is finite set

((I,A) . B) \ ((I,A,B) . B) is finite set

A . B is set

{(A . B)} is non empty finite set

{(A . B)} \ ((I,A,B) . B) is finite set

B . B is set

{(A . B),(B . B)} is non empty finite set

{(A . B)} \ {(A . B),(B . B)} is finite set

([[0]] I) . B is set

B is set

((I,B) \ (I,A,B)) . B is set

(I,B) . B is finite set

(I,A,B) . B is finite set

((I,B) . B) \ ((I,A,B) . B) is finite set

B . B is set

{(B . B)} is non empty finite set

{(B . B)} \ ((I,A,B) . B) is finite set

A . B is set

{(A . B),(B . B)} is non empty finite set

{(B . B)} \ {(A . B),(B . B)} is finite set

([[0]] I) . B is set

I is set

A is Relation-like I -defined Function-like V14(I) set

(I,A) is Relation-like non-empty I -defined Function-like V14(I) finite-yielding set

B is Relation-like I -defined Function-like V14(I) set

(I,B) is Relation-like non-empty I -defined Function-like V14(I) finite-yielding set

B is set

(I,A) . B is finite set

(I,B) . B is finite set

A . B is set

{(A . B)} is non empty finite set

B . B is set

{(B . B)} is non empty finite set

I is set

A is Relation-like I -defined Function-like V14(I) set

B is Relation-like I -defined Function-like V14(I) set

(I,A,B) is Relation-like non-empty I -defined Function-like V14(I) finite-yielding set

B is Relation-like I -defined Function-like V14(I) set

(I,B) is Relation-like non-empty I -defined Function-like V14(I) finite-yielding set

y is set

(I,A,B) . y is finite set

(I,B) . y is finite set

B . y is set

{(B . y)} is non empty finite set

A . y is set

B . y is set

{(A . y),(B . y)} is non empty finite set

y is set

(I,A,B) . y is finite set

(I,B) . y is finite set

B . y is set

{(B . y)} is non empty finite set

A . y is set

B . y is set

{(A . y),(B . y)} is non empty finite set

I is set

A is Relation-like I -defined Function-like V14(I) set

B is Relation-like I -defined Function-like V14(I) set

(I,A,B) is Relation-like non-empty I -defined Function-like V14(I) finite-yielding set

B is Relation-like I -defined Function-like V14(I) set

(I,B) is Relation-like non-empty I -defined Function-like V14(I) finite-yielding set

y is set

(I,A,B) . y is finite set

(I,B) . y is finite set

A . y is set

B . y is set

{(A . y),(B . y)} is non empty finite set

B . y is set

{(B . y)} is non empty finite set

I is set

[[0]] I is Relation-like I -defined Function-like V14(I) set

I --> {} is Relation-like I -defined Function-like constant V14(I) V18(I,{{}}) M2( bool [:I,{{}}:])

{{}} is non empty finite V29() set

[:I,{{}}:] is set

bool [:I,{{}}:] is set

A is Relation-like I -defined Function-like V14(I) set

(I,A) is Relation-like non-empty I -defined Function-like V14(I) finite-yielding set

bool (I,A) is Relation-like I -defined Function-like V14(I) set

(I,([[0]] I),(I,A)) is Relation-like non-empty I -defined Function-like V14(I) finite-yielding set

B is set

(bool (I,A)) . B is set

(I,A) . B is finite set

bool ((I,A) . B) is finite V29() set

A . B is set

{(A . B)} is non empty finite set

bool {(A . B)} is finite V29() set

{{},{(A . B)}} is non empty finite V29() set

([[0]] I) . B is set

{(([[0]] I) . B),{(A . B)}} is non empty finite set

{(([[0]] I) . B),((I,A) . B)} is non empty finite set

(I,([[0]] I),(I,A)) . B is finite set

I is set

A is Relation-like I -defined Function-like V14(I) set

(I,A) is Relation-like non-empty I -defined Function-like V14(I) finite-yielding set

bool A is Relation-like I -defined Function-like V14(I) set

B is set

(I,A) . B is finite set

(bool A) . B is set

A . B is set

{(A . B)} is non empty finite set

bool (A . B) is set

I is set

A is Relation-like I -defined Function-like V14(I) set

(I,A) is Relation-like non-empty I -defined Function-like V14(I) finite-yielding set

union (I,A) is Relation-like I -defined Function-like V14(I) set

B is set

(union (I,A)) . B is set

(I,A) . B is finite set

union ((I,A) . B) is set

A . B is set

{(A . B)} is non empty finite set

union {(A . B)} is set

I is set

A is Relation-like I -defined Function-like V14(I) set

(I,A) is Relation-like non-empty I -defined Function-like V14(I) finite-yielding set

B is Relation-like I -defined Function-like V14(I) set

(I,B) is Relation-like non-empty I -defined Function-like V14(I) finite-yielding set

(I,(I,A),(I,B)) is Relation-like non-empty I -defined Function-like V14(I) finite-yielding set

union (I,(I,A),(I,B)) is Relation-like I -defined Function-like V14(I) set

(I,A,B) is Relation-like non-empty I -defined Function-like V14(I) finite-yielding set

B is set

(union (I,(I,A),(I,B))) . B is set

(I,(I,A),(I,B)) . B is finite set

union ((I,(I,A),(I,B)) . B) is set

(I,A) . B is finite set

(I,B) . B is finite set

{((I,A) . B),((I,B) . B)} is non empty finite V29() set

union {((I,A) . B),((I,B) . B)} is finite set

A . B is set

{(A . B)} is non empty finite set

{{(A . B)},((I,B) . B)} is non empty finite V29() set

union {{(A . B)},((I,B) . B)} is finite set

B . B is set

{(B . B)} is non empty finite set

{{(A . B)},{(B . B)}} is non empty finite V29() set

union {{(A . B)},{(B . B)}} is finite set

{(A . B),(B . B)} is non empty finite set

(I,A,B) . B is finite set

I is set

A is Relation-like I -defined Function-like V14(I) set

B is Relation-like I -defined Function-like V14(I) set

(I,A,B) is Relation-like non-empty I -defined Function-like V14(I) finite-yielding set

union (I,A,B) is Relation-like I -defined Function-like V14(I) set

A \/ B is Relation-like I -defined Function-like V14(I) set

B is set

(union (I,A,B)) . B is set

(I,A,B) . B is finite set

union ((I,A,B) . B) is set

A . B is set

B . B is set

{(A . B),(B . B)} is non empty finite set

union {(A . B),(B . B)} is set

(A . B) \/ (B . B) is set

(A \/ B) . B is set

I is set

A is Relation-like I -defined Function-like V14(I) set

(I,A) is Relation-like non-empty I -defined Function-like V14(I) finite-yielding set

B is Relation-like I -defined Function-like V14(I) set

B is set

A . B is set

B . B is set

(I,A) . B is finite set

{(A . B)} is non empty finite set

B is set

(I,A) . B is finite set

B . B is set

A . B is set

{(A . B)} is non empty finite set

I is set

A is Relation-like I -defined Function-like V14(I) set

B is Relation-like I -defined Function-like V14(I) set

(I,A,B) is Relation-like non-empty I -defined Function-like V14(I) finite-yielding set

B is Relation-like I -defined Function-like V14(I) set

y is set

A . y is set

B . y is set

(I,A,B) . y is finite set

B . y is set

{(A . y),(B . y)} is non empty finite set

y is set

B . y is set

B . y is set

(I,A,B) . y is finite set

A . y is set

{(A . y),(B . y)} is non empty finite set

y is set

(I,A,B) . y is finite set

B . y is set

A . y is set

B . y is set

{(A . y),(B . y)} is non empty finite set

I is set

[[0]] I is Relation-like I -defined Function-like V14(I) set

I --> {} is Relation-like I -defined Function-like constant V14(I) V18(I,{{}}) M2( bool [:I,{{}}:])

{{}} is non empty finite V29() set

[:I,{{}}:] is set

bool [:I,{{}}:] is set

A is Relation-like I -defined Function-like V14(I) set

B is Relation-like I -defined Function-like V14(I) set

(I,B) is Relation-like non-empty I -defined Function-like V14(I) finite-yielding set

B is Relation-like I -defined Function-like V14(I) set

(I,B) is Relation-like non-empty I -defined Function-like V14(I) finite-yielding set

(I,B,B) is Relation-like non-empty I -defined Function-like V14(I) finite-yielding set

y is set

A . y is set

(I,B,B) . y is finite set

B . y is set

B . y is set

{(B . y),(B . y)} is non empty finite set

B . y is set

{(B . y)} is non empty finite set

B . y is set

{(B . y),(B . y)} is non empty finite set

B . y is set

{(B . y)} is non empty finite set

B . y is set

{(B . y),(B . y)} is non empty finite set

I is set

A is Relation-like I -defined Function-like V14(I) set

B is Relation-like I -defined Function-like V14(I) set

B is Relation-like I -defined Function-like V14(I) set

(I,B) is Relation-like non-empty I -defined Function-like V14(I) finite-yielding set

B \/ (I,B) is Relation-like I -defined Function-like V14(I) set

y is set

A . y is set

(B \/ (I,B)) . y is set

B . y is set

B . y is set

{(B . y)} is non empty finite set

(B . y) \/ {(B . y)} is non empty set

(I,B) . y is finite set

(B . y) \/ ((I,B) . y) is set

B . y is set

B . y is set

{(B . y)} is non empty finite set

(B . y) \/ {(B . y)} is non empty set

(I,B) . y is finite set

(B . y) \/ ((I,B) . y) is set

I is set

A is Relation-like I -defined Function-like V14(I) set

B is Relation-like I -defined Function-like V14(I) set

(I,B) is Relation-like non-empty I -defined Function-like V14(I) finite-yielding set

A \/ (I,B) is Relation-like I -defined Function-like V14(I) set

B is Relation-like I -defined Function-like V14(I) set

y is set

(A \/ (I,B)) . y is set

B . y is set

A . y is set

(I,B) . y is finite set

(A . y) \/ ((I,B) . y) is set

B . y is set

{(B . y)} is non empty finite set

(A . y) \/ {(B . y)} is non empty set

y is set

B . y is set

B . y is set

A . y is set

{(B . y)} is non empty finite set

(A . y) \/ {(B . y)} is non empty set

y is set

A . y is set

B . y is set

B . y is set

{(B . y)} is non empty finite set

(A . y) \/ {(B . y)} is non empty set

y is set

(A \/ (I,B)) . y is set

B . y is set

B . y is set

A . y is set

{(B . y)} is non empty finite set

(A . y) \/ {(B . y)} is non empty set

(I,B) . y is finite set

(A . y) \/ ((I,B) . y) is set

I is set

A is Relation-like I -defined Function-like V14(I) set

(I,A) is Relation-like non-empty I -defined Function-like V14(I) finite-yielding set

B is Relation-like I -defined Function-like V14(I) set

(I,A) \/ B is Relation-like I -defined Function-like V14(I) set

B is set

A . B is set

B . B is set

{(A . B)} is non empty finite set

{(A . B)} \/ (B . B) is non empty set

(I,A) . B is finite set

((I,A) . B) \/ (B . B) is set

I is set

A is Relation-like I -defined Function-like V14(I) set

(I,A) is Relation-like non-empty I -defined Function-like V14(I) finite-yielding set

B is Relation-like I -defined Function-like V14(I) set

(I,A) \/ B is Relation-like I -defined Function-like V14(I) set

B is set

A . B is set

B . B is set

((I,A) \/ B) . B is set

(I,A) . B is finite set

((I,A) . B) \/ (B . B) is set

{(A . B)} is non empty finite set

{(A . B)} \/ (B . B) is non empty set

I is set

A is Relation-like I -defined Function-like V14(I) set

B is Relation-like I -defined Function-like V14(I) set

(I,A,B) is Relation-like non-empty I -defined Function-like V14(I) finite-yielding set

B is Relation-like I -defined Function-like V14(I) set

(I,A,B) \/ B is Relation-like I -defined Function-like V14(I) set

y is set

A . y is set

B . y is set

B . y is set

{(A . y),(B . y)} is non empty finite set

{(A . y),(B . y)} \/ (B . y) is non empty set

(I,A,B) . y is finite set

((I,A,B) . y) \/ (B . y) is set

y is set

B . y is set

B . y is set

A . y is set

{(A . y),(B . y)} is non empty finite set

{(A . y),(B . y)} \/ (B . y) is non empty set

(I,A,B) . y is finite set

((I,A,B) . y) \/ (B . y) is set

y is set

A . y is set

B . y is set

B . y is set

((I,A,B) \/ B) . y is set

(I,A,B) . y is finite set

((I,A,B) . y) \/ (B . y) is set

{(A . y),(B . y)} is non empty finite set

{(A . y),(B . y)} \/ (B . y) is non empty set

I is set

[[0]] I is Relation-like I -defined Function-like V14(I) set

I --> {} is Relation-like I -defined Function-like constant V14(I) V18(I,{{}}) M2( bool [:I,{{}}:])

{{}} is non empty finite V29() set

[:I,{{}}:] is set

bool [:I,{{}}:] is set

A is Relation-like I -defined Function-like V14(I) set

(I,A) is Relation-like non-empty I -defined Function-like V14(I) finite-yielding set

B is Relation-like I -defined Function-like V14(I) set

(I,A) \/ B is Relation-like I -defined Function-like V14(I) set

B is set

A . B is set

{(A . B)} is non empty finite set

B . B is set

{(A . B)} \/ (B . B) is non empty set

(I,A) . B is finite set

((I,A) . B) \/ (B . B) is set

((I,A) \/ B) . B is set

I is set

[[0]] I is Relation-like I -defined Function-like V14(I) set

I --> {} is Relation-like I -defined Function-like constant V14(I) V18(I,{{}}) M2( bool [:I,{{}}:])

{{}} is non empty finite V29() set

[:I,{{}}:] is set

bool [:I,{{}}:] is set

A is Relation-like I -defined Function-like V14(I) set

B is Relation-like I -defined Function-like V14(I) set

(I,A,B) is Relation-like non-empty I -defined Function-like V14(I) finite-yielding set

B is Relation-like I -defined Function-like V14(I) set

(I,A,B) \/ B is Relation-like I -defined Function-like V14(I) set

y is set

A . y is set

B . y is set

{(A . y),(B . y)} is non empty finite set

B . y is set

{(A . y),(B . y)} \/ (B . y) is non empty set

(I,A,B) . y is finite set

((I,A,B) . y) \/ (B . y) is set

((I,A,B) \/ B) . y is set

I is set

A is Relation-like I -defined Function-like V14(I) set

B is Relation-like I -defined Function-like V14(I) set

(I,B) is Relation-like non-empty I -defined Function-like V14(I) finite-yielding set

A /\ (I,B) is Relation-like I -defined Function-like V14(I) set

B is set

B . B is set

A . B is set

{(B . B)} is non empty finite set

(A . B) /\ {(B . B)} is finite set

(I,B) . B is finite set

(A . B) /\ ((I,B) . B) is finite set

(A /\ (I,B)) . B is set

I is set

A is Relation-like I -defined Function-like V14(I) set

(I,A) is Relation-like non-empty I -defined Function-like V14(I) finite-yielding set

B is Relation-like I -defined Function-like V14(I) set

B /\ (I,A) is Relation-like I -defined Function-like V14(I) set

B is set

A . B is set

B . B is set

(B /\ (I,A)) . B is set

(I,A) . B is finite set

(B . B) /\ ((I,A) . B) is finite set

{(A . B)} is non empty finite set

(B . B) /\ {(A . B)} is finite set

I is set

A is Relation-like I -defined Function-like V14(I) set

B is Relation-like I -defined Function-like V14(I) set

B is Relation-like I -defined Function-like V14(I) set

(I,A,B) is Relation-like non-empty I -defined Function-like V14(I) finite-yielding set

(I,A,B) /\ B is Relation-like I -defined Function-like V14(I) set

y is set

A . y is set

B . y is set

B . y is set

((I,A,B) /\ B) . y is set

(I,A,B) . y is finite set

((I,A,B) . y) /\ (B . y) is finite set

{(A . y),(B . y)} is non empty finite set

{(A . y),(B . y)} /\ (B . y) is finite set

y is set

A . y is set

B . y is set

B . y is set

{(A . y),(B . y)} is non empty finite set

{(A . y),(B . y)} /\ (B . y) is finite set

(I,A,B) . y is finite set

((I,A,B) . y) /\ (B . y) is finite set

((I,A,B) /\ B) . y is set

y is set

B . y is set

B . y is set

A . y is set

{(A . y),(B . y)} is non empty finite set

{(A . y),(B . y)} /\ (B . y) is finite set

(I,A,B) . y is finite set

((I,A,B) . y) /\ (B . y) is finite set

((I,A,B) /\ B) . y is set

I is set

[[0]] I is Relation-like I -defined Function-like V14(I) set

I --> {} is Relation-like I -defined Function-like constant V14(I) V18(I,{{}}) M2( bool [:I,{{}}:])

{{}} is non empty finite V29() set

[:I,{{}}:] is set

bool [:I,{{}}:] is set

A is Relation-like I -defined Function-like V14(I) set

(I,A) is Relation-like non-empty I -defined Function-like V14(I) finite-yielding set

B is Relation-like I -defined Function-like V14(I) set

(I,A) /\ B is Relation-like I -defined Function-like V14(I) set

B is set

A . B is set

{(A . B)} is non empty finite set

B . B is set

{(A . B)} /\ (B . B) is finite set

(I,A) . B is finite set

((I,A) . B) /\ (B . B) is finite set

((I,A) /\ B) . B is set

I is set

[[0]] I is Relation-like I -defined Function-like V14(I) set

I --> {} is Relation-like I -defined Function-like constant V14(I) V18(I,{{}}) M2( bool [:I,{{}}:])

{{}} is non empty finite V29() set

[:I,{{}}:] is set

bool [:I,{{}}:] is set

A is Relation-like I -defined Function-like V14(I) set

B is Relation-like I -defined Function-like V14(I) set

(I,A,B) is Relation-like non-empty I -defined Function-like V14(I) finite-yielding set

B is Relation-like I -defined Function-like V14(I) set

(I,A,B) /\ B is Relation-like I -defined Function-like V14(I) set

y is set

A . y is set

B . y is set

{(A . y),(B . y)} is non empty finite set

B . y is set

{(A . y),(B . y)} /\ (B . y) is finite set

(I,A,B) . y is finite set

((I,A,B) . y) /\ (B . y) is finite set

((I,A,B) /\ B) . y is set

y is set

X is set

A . X is set

B . X is set

{(A . X),(B . X)} is non empty finite set

B . X is set

{(A . X),(B . X)} /\ (B . X) is finite set

y is set

A . y is set

B . y is set

y is set

X is set

A . X is set

B . X is set

{(A . X),(B . X)} is non empty finite set

B . X is set

{(A . X),(B . X)} /\ (B . X) is finite set

y is set

B . y is set

B . y is set

I is set

A is Relation-like I -defined Function-like V14(I) set

B is Relation-like I -defined Function-like V14(I) set

B is Relation-like I -defined Function-like V14(I) set

(I,B) is Relation-like non-empty I -defined Function-like V14(I) finite-yielding set

B \ (I,B) is Relation-like I -defined Function-like V14(I) set

y is set

A . y is set

B . y is set

(B \ (I,B)) . y is set

(I,B) . y is finite set

(B . y) \ ((I,B) . y) is set

B . y is set

{(B . y)} is non empty finite set

(B . y) \ {(B . y)} is set

I is set

A is Relation-like I -defined Function-like V14(I) set

B is Relation-like I -defined Function-like V14(I) set

B is Relation-like I -defined Function-like V14(I) set

(I,B) is Relation-like non-empty I -defined Function-like V14(I) finite-yielding set

B \ (I,B) is Relation-like I -defined Function-like V14(I) set

y is set

X is set

A . X is set

(B \ (I,B)) . X is set

B . X is set

(I,B) . X is finite set

(B . X) \ ((I,B) . X) is set

B . X is set

{(B . X)} is non empty finite set

(B . X) \ {(B . X)} is set

X is set

A . X is set

B . X is set

I is set

A is Relation-like I -defined Function-like V14(I) set

B is Relation-like I -defined Function-like V14(I) set

(I,B) is Relation-like non-empty I -defined Function-like V14(I) finite-yielding set

A \ (I,B) is Relation-like I -defined Function-like V14(I) set

B is set

A . B is set

B . B is set

{(B . B)} is non empty finite set

(A . B) \ {(B . B)} is set

(I,B) . B is finite set

(A . B) \ ((I,B) . B) is set

B is set

y is set

A . y is set

B . y is set

{(B . y)} is non empty finite set

(A . y) \ {(B . y)} is set

B is set

B . B is set

A . B is set

I is set

A is Relation-like I -defined Function-like V14(I) set

(I,A) is Relation-like non-empty I -defined Function-like V14(I) finite-yielding set

B is Relation-like I -defined Function-like V14(I) set

(I,A) \ B is Relation-like I -defined Function-like V14(I) set

B is set

A . B is set

{(A . B)} is non empty finite set

B . B is set

{(A . B)} \ (B . B) is finite set

(I,A) . B is finite set

((I,A) . B) \ (B . B) is finite set

((I,A) \ B) . B is set

I is set

[[0]] I is Relation-like I -defined Function-like V14(I) set

I --> {} is Relation-like I -defined Function-like constant V14(I) V18(I,{{}}) M2( bool [:I,{{}}:])

{{}} is non empty finite V29() set

[:I,{{}}:] is set

bool [:I,{{}}:] is set

A is Relation-like I -defined Function-like V14(I) set

(I,A) is Relation-like non-empty I -defined Function-like V14(I) finite-yielding set

B is Relation-like I -defined Function-like V14(I) set

(I,A) \ B is Relation-like I -defined Function-like V14(I) set

B is set

A . B is set

B . B is set

{(A . B)} is non empty finite set

{(A . B)} \ (B . B) is finite set

(I,A) . B is finite set

((I,A) . B) \ (B . B) is finite set

((I,A) \ B) . B is set

B is set

A . B is set

B . B is set

((I,A) \ B) . B is set

(I,A) . B is finite set

((I,A) . B) \ (B . B) is finite set

{(A . B)} is non empty finite set

{(A . B)} \ (B . B) is finite set

([[0]] I) . B is set

I is set

A is Relation-like I -defined Function-like V14(I) set

(I,A) is Relation-like non-empty I -defined Function-like V14(I) finite-yielding set

B is Relation-like I -defined Function-like V14(I) set

(I,A,B) is Relation-like non-empty I -defined Function-like V14(I) finite-yielding set

B is Relation-like I -defined Function-like V14(I) set

(I,A,B) \ B is Relation-like I -defined Function-like V14(I) set

y is set

A . y is set

B . y is set

{(A . y),(B . y)} is non empty finite set

B . y is set

{(A . y),(B . y)} \ (B . y) is finite set

(I,A,B) . y is finite set

((I,A,B) . y) \ (B . y) is finite set

((I,A,B) \ B) . y is set

{(A . y)} is non empty finite set

I is set

A is Relation-like I -defined Function-like V14(I) set

B is Relation-like I -defined Function-like V14(I) set

(I,A,B) is Relation-like non-empty I -defined Function-like V14(I) finite-yielding set

B is Relation-like I -defined Function-like V14(I) set

(I,A,B) \ B is Relation-like I -defined Function-like V14(I) set

y is set

A . y is set

B . y is set

{(A . y),(B . y)} is non empty finite set

B . y is set

{(A . y),(B . y)} \ (B . y) is finite set

(I,A,B) . y is finite set

((I,A,B) . y) \ (B . y) is finite set

((I,A,B) \ B) . y is set

A . y is set

B . y is set

{(A . y),(B . y)} is non empty finite set

B . y is set

{(A . y),(B . y)} \ (B . y) is finite set

(I,A,B) . y is finite set

((I,A,B) . y) \ (B . y) is finite set

((I,A,B) \ B) . y is set

I is set

[[0]] I is Relation-like I -defined Function-like V14(I) set

I --> {} is Relation-like I -defined Function-like constant V14(I) V18(I,{{}}) M2( bool [:I,{{}}:])

{{}} is non empty finite V29() set

[:I,{{}}:] is set

bool [:I,{{}}:] is set

A is Relation-like I -defined Function-like V14(I) set

B is Relation-like I -defined Function-like V14(I) set

(I,A,B) is Relation-like non-empty I -defined Function-like V14(I) finite-yielding set

B is Relation-like I -defined Function-like V14(I) set

(I,A,B) \ B is Relation-like I -defined Function-like V14(I) set

y is set

A . y is set

B . y is set

B . y is set

{(A . y),(B . y)} is non empty finite set

{(A . y),(B . y)} \ (B . y) is finite set

(I,A,B) . y is finite set

((I,A,B) . y) \ (B . y) is finite set

((I,A,B) \ B) . y is set

y is set

B . y is set

B . y is set

A . y is set

{(A . y),(B . y)} is non empty finite set

{(A . y),(B . y)} \ (B . y) is finite set

(I,A,B) . y is finite set

((I,A,B) . y) \ (B . y) is finite set

((I,A,B) \ B) . y is set

y is set

A . y is set

B . y is set

B . y is set

((I,A,B) \ B) . y is set

(I,A,B) . y is finite set

((I,A,B) . y) \ (B . y) is finite set

{(A . y),(B . y)} is non empty finite set

{(A . y),(B . y)} \ (B . y) is finite set

([[0]] I) . y is set

I is set

[[0]] I is Relation-like I -defined Function-like V14(I) set

I --> {} is Relation-like I -defined Function-like constant V14(I) V18(I,{{}}) M2( bool [:I,{{}}:])

{{}} is non empty finite V29() set

[:I,{{}}:] is set

bool [:I,{{}}:] is set

A is Relation-like I -defined Function-like V14(I) set

B is Relation-like I -defined Function-like V14(I) set

(I,B) is Relation-like non-empty I -defined Function-like V14(I) finite-yielding set

B is Relation-like I -defined Function-like V14(I) set

(I,B) is Relation-like non-empty I -defined Function-like V14(I) finite-yielding set

(I,B,B) is Relation-like non-empty I -defined Function-like V14(I) finite-yielding set

A \ (I,B,B) is Relation-like I -defined Function-like V14(I) set

y is set

A . y is set

(A \ (I,B,B)) . y is set

(I,B,B) . y is finite set

(A . y) \ ((I,B,B) . y) is set

([[0]] I) . y is set

A . y is set

B . y is set

{(B . y)} is non empty finite set

(A \ (I,B,B)) . y is set

(I,B,B) . y is finite set

(A . y) \ ((I,B,B) . y) is set

B . y is set

{(B . y),(B . y)} is non empty finite set

(A . y) \ {(B . y),(B . y)} is set

([[0]] I) . y is set

A . y is set

B . y is set

{(B . y)} is non empty finite set

(A \ (I,B,B)) . y is set

(I,B,B) . y is finite set

(A . y) \ ((I,B,B) . y) is set

B . y is set

{(B . y),(B . y)} is non empty finite set

(A . y) \ {(B . y),(B . y)} is set

([[0]] I) . y is set

A . y is set

B . y is set

B . y is set

{(B . y),(B . y)} is non empty finite set

(A \ (I,B,B)) . y is set

(I,B,B) . y is finite set

(A . y) \ ((I,B,B) . y) is set

(A . y) \ {(B . y),(B . y)} is set

([[0]] I) . y is set

I is set

[[0]] I is Relation-like I -defined Function-like V14(I) set

I --> {} is Relation-like I -defined Function-like constant V14(I) V18(I,{{}}) M2( bool [:I,{{}}:])

{{}} is non empty finite V29() set

[:I,{{}}:] is set

bool [:I,{{}}:] is set

A is Relation-like I -defined Function-like V14(I) set

B is Relation-like I -defined Function-like V14(I) set

[|A,B|] is Relation-like I -defined Function-like V14(I) set

B is set

A . B is set

[|A,B|] . B is set

B . B is set

[:(A . B),(B . B):] is set

([[0]] I) . B is set

B is set

B . B is set

[|A,B|] . B is set

A . B is set

[:(A . B),(B . B):] is set

([[0]] I) . B is set

I is set

A is Relation-like I -defined Function-like V14(I) set

B is Relation-like I -defined Function-like V14(I) set

[|A,B|] is Relation-like I -defined Function-like V14(I) set

[|B,A|] is Relation-like I -defined Function-like V14(I) set

B is set

A . B is set

B . B is set

[:(A . B),(B . B):] is set

[|A,B|] . B is set

[:(B . B),(A . B):] is set

I is set

A is Relation-like I -defined Function-like V14(I) set

[|A,A|] is Relation-like I -defined Function-like V14(I) set

B is Relation-like I -defined Function-like V14(I) set

[|B,B|] is Relation-like I -defined Function-like V14(I) set

B is set

A . B is set

[:(A . B),(A . B):] is set

[|A,A|] . B is set

B . B is set

[:(B . B),(B . B):] is set

I is set

A is Relation-like I -defined Function-like V14(I) set

B is Relation-like I -defined Function-like V14(I) set

[|B,A|] is Relation-like I -defined Function-like V14(I) set

[|A,B|] is Relation-like I -defined Function-like V14(I) set

B is Relation-like I -defined Function-like V14(I) set

[|B,A|] is Relation-like I -defined Function-like V14(I) set

[|A,B|] is Relation-like I -defined Function-like V14(I) set

y is set

B . y is set

B . y is set

A . y is set

[|B,A|] . y is set

[|B,A|] . y is set

[:(B . y),(A . y):] is set

[:(B . y),(A . y):] is set

y is set

B . y is set

B . y is set

A . y is set

[|A,B|] . y is set

[|A,B|] . y is set

[:(A . y),(B . y):] is set

[:(A . y),(B . y):] is set

I is set

A is Relation-like I -defined Function-like V14(I) set

B is Relation-like I -defined Function-like V14(I) set

B is Relation-like I -defined Function-like V14(I) set

[|A,B|] is Relation-like I -defined Function-like V14(I) set

[|B,B|] is Relation-like I -defined Function-like V14(I) set

[|B,A|] is Relation-like I -defined Function-like V14(I) set

[|B,B|] is Relation-like I -defined Function-like V14(I) set

y is set

[|A,B|] . y is set

[|B,B|] . y is set

A . y is set

B . y is set

B . y is set

[:(A . y),(B . y):] is set

[:(B . y),(B . y):] is set

y is set

[|B,A|] . y is set

[|B,B|] . y is set

A . y is set

B . y is set

B . y is set

[:(B . y),(A . y):] is set

[:(B . y),(B . y):] is set

I is set

A is Relation-like I -defined Function-like V14(I) set

B is Relation-like I -defined Function-like V14(I) set

B is Relation-like I -defined Function-like V14(I) set

[|A,B|] is Relation-like I -defined Function-like V14(I) set

y is Relation-like I -defined Function-like V14(I) set

[|B,y|] is Relation-like I -defined Function-like V14(I) set

X is set

[|A,B|] . X is set

[|B,y|] . X is set

A . X is set

B . X is set

B . X is set

y . X is set

[:(A . X),(B . X):] is set

[:(B . X),(y . X):] is set

I is set

A is Relation-like I -defined Function-like V14(I) set

B is Relation-like I -defined Function-like V14(I) set

A \/ B is Relation-like I -defined Function-like V14(I) set

B is Relation-like I -defined Function-like V14(I) set

[|(A \/ B),B|] is Relation-like I -defined Function-like V14(I) set

[|A,B|] is Relation-like I -defined Function-like V14(I) set

[|B,B|] is Relation-like I -defined Function-like V14(I) set

[|A,B|] \/ [|B,B|] is Relation-like I -defined Function-like V14(I) set

[|B,(A \/ B)|] is Relation-like I -defined Function-like V14(I) set

[|B,A|] is Relation-like I -defined Function-like V14(I) set

[|B,B|] is Relation-like I -defined Function-like V14(I) set

[|B,A|] \/ [|B,B|] is Relation-like I -defined Function-like V14(I) set

y is set

[|(A \/ B),B|] . y is set

(A \/ B) . y is set

B . y is set

[:((A \/ B) . y),(B . y):] is set

A . y is set

B . y is set

(A . y) \/ (B . y) is set

[:((A . y) \/ (B . y)),(B . y):] is set

[:(A . y),(B . y):] is set

[:(B . y),(B . y):] is set

[:(A . y),(B . y):] \/ [:(B . y),(B . y):] is set

[|A,B|] . y is set

([|A,B|] . y) \/ [:(B . y),(B . y):] is set

[|B,B|] . y is set

([|A,B|] . y) \/ ([|B,B|] . y) is set

([|A,B|] \/ [|B,B|]) . y is set

y is set

[|B,(A \/ B)|] . y is set

B . y is set

(A \/ B) . y is set

[:(B . y),((A \/ B) . y):] is set

A . y is set

B . y is set

(A . y) \/ (B . y) is set

[:(B . y),((A . y) \/ (B . y)):] is set

[:(B . y),(A . y):] is set

[:(B . y),(B . y):] is set

[:(B . y),(A . y):] \/ [:(B . y),(B . y):] is set

[|B,A|] . y is set

([|B,A|] . y) \/ [:(B . y),(B . y):] is set

[|B,B|] . y is set

([|B,A|] . y) \/ ([|B,B|] . y) is set

([|B,A|] \/ [|B,B|]) . y is set

I is set

A is Relation-like I -defined Function-like V14(I) set

B is Relation-like I -defined Function-like V14(I) set

A \/ B is Relation-like I -defined Function-like V14(I) set

B is Relation-like I -defined Function-like V14(I) set

[|A,B|] is Relation-like I -defined Function-like V14(I) set

[|B,B|] is Relation-like I -defined Function-like V14(I) set

y is Relation-like I -defined Function-like V14(I) set

B \/ y is Relation-like I -defined Function-like V14(I) set

[|(A \/ B),(B \/ y)|] is Relation-like I -defined Function-like V14(I) set

[|A,y|] is Relation-like I -defined Function-like V14(I) set

[|A,B|] \/ [|A,y|] is Relation-like I -defined Function-like V14(I) set

([|A,B|] \/ [|A,y|]) \/ [|B,B|] is Relation-like I -defined Function-like V14(I) set

[|B,y|] is Relation-like I -defined Function-like V14(I) set

(([|A,B|] \/ [|A,y|]) \/ [|B,B|]) \/ [|B,y|] is Relation-like I -defined Function-like V14(I) set

X is set

[|(A \/ B),(B \/ y)|] . X is set

(A \/ B) . X is set

(B \/ y) . X is set

[:((A \/ B) . X),((B \/ y) . X):] is set

A . X is set

B . X is set

(A . X) \/ (B . X) is set

[:((A . X) \/ (B . X)),((B \/ y) . X):] is set

B . X is set

y . X is set

(B . X) \/ (y . X) is set

[:((A . X) \/ (B . X)),((B . X) \/ (y . X)):] is set

[:(A . X),(B . X):] is set

[:(A . X),(y . X):] is set

[:(A . X),(B . X):] \/ [:(A . X),(y . X):] is set

[:(B . X),(B . X):] is set

([:(A . X),(B . X):] \/ [:(A . X),(y . X):]) \/ [:(B . X),(B . X):] is set

[:(B . X),(y . X):] is set

(([:(A . X),(B . X):] \/ [:(A . X),(y . X):]) \/ [:(B . X),(B . X):]) \/ [:(B . X),(y . X):] is set

[|A,B|] . X is set

([|A,B|] . X) \/ [:(A . X),(y . X):] is set

(([|A,B|] . X) \/ [:(A . X),(y . X):]) \/ [:(B . X),(B . X):] is set

((([|A,B|] . X) \/ [:(A . X),(y . X):]) \/ [:(B . X),(B . X):]) \/ [:(B . X),(y . X):] is set

[|A,y|] . X is set

([|A,B|] . X) \/ ([|A,y|] . X) is set

(([|A,B|] . X) \/ ([|A,y|] . X)) \/ [:(B . X),(B . X):] is set

((([|A,B|] . X) \/ ([|A,y|] . X)) \/ [:(B . X),(B . X):]) \/ [:(B . X),(y . X):] is set

[|B,B|] . X is set

(([|A,B|] . X) \/ ([|A,y|] . X)) \/ ([|B,B|] . X) is set

((([|A,B|] . X) \/ ([|A,y|] . X)) \/ ([|B,B|] . X)) \/ [:(B . X),(y . X):] is set

[|B,y|] . X is set

((([|A,B|] . X) \/ ([|A,y|] . X)) \/ ([|B,B|] . X)) \/ ([|B,y|] . X) is