:: PETRI_2 semantic presentation

K195() is Element of bool K191()

K191() is set

bool K191() is non empty set

K120() is set

bool K120() is non empty set

bool K195() is non empty set

K270() is set

{} is empty trivial Relation-like non-empty empty-yielding Function-like one-to-one constant functional finite finite-yielding V32() set

1 is non empty set

O is set

CPNT1 is non empty set

[:O,CPNT1:] is Relation-like set

bool [:O,CPNT1:] is non empty set

CPNT2 is set

[:CPNT2,CPNT1:] is Relation-like set

bool [:CPNT2,CPNT1:] is non empty set

q is Relation-like O -defined CPNT1 -valued Function-like total quasi_total Element of bool [:O,CPNT1:]

{ b

Funcs (CPNT2,CPNT1) is non empty functional FUNCTION_DOMAIN of CPNT2,CPNT1

bool (Funcs (CPNT2,CPNT1)) is non empty set

the Relation-like CPNT2 -defined CPNT1 -valued Function-like total quasi_total Element of bool [:CPNT2,CPNT1:] is Relation-like CPNT2 -defined CPNT1 -valued Function-like total quasi_total Element of bool [:CPNT2,CPNT1:]

the Relation-like CPNT2 -defined CPNT1 -valued Function-like total quasi_total Element of bool [:CPNT2,CPNT1:] | {} is empty trivial Relation-like non-empty empty-yielding {} -defined CPNT2 -defined CPNT1 -valued Function-like one-to-one constant functional finite finite-yielding V32() Element of bool [:CPNT2,CPNT1:]

CB is set

q . CB is set

{(q . CB)} is non empty trivial finite set

CPNT2 --> (q . CB) is Relation-like CPNT2 -defined {(q . CB)} -valued Function-like total quasi_total Element of bool [:CPNT2,{(q . CB)}:]

[:CPNT2,{(q . CB)}:] is Relation-like set

bool [:CPNT2,{(q . CB)}:] is non empty set

(CPNT2 --> (q . CB)) +* q is Relation-like Function-like set

rng ((CPNT2 --> (q . CB)) +* q) is set

rng (CPNT2 --> (q . CB)) is set

rng q is set

(rng (CPNT2 --> (q . CB))) \/ (rng q) is set

dom q is Element of bool O

bool O is non empty set

dom ((CPNT2 --> (q . CB)) +* q) is set

dom (CPNT2 --> (q . CB)) is Element of bool CPNT2

bool CPNT2 is non empty set

(dom (CPNT2 --> (q . CB))) \/ O is set

CPNT2 \/ O is set

q21A is Relation-like CPNT2 -defined CPNT1 -valued Function-like total quasi_total Element of bool [:CPNT2,CPNT1:]

q21A | O is Relation-like O -defined CPNT2 -defined CPNT1 -valued Function-like Element of bool [:CPNT2,CPNT1:]

CB is set

q12A is Relation-like CPNT2 -defined CPNT1 -valued Function-like total quasi_total Element of bool [:CPNT2,CPNT1:]

q12A | O is Relation-like O -defined CPNT2 -defined CPNT1 -valued Function-like Element of bool [:CPNT2,CPNT1:]

CPNT2 is set

CPNT1 is non empty set

Funcs (CPNT2,CPNT1) is non empty functional FUNCTION_DOMAIN of CPNT2,CPNT1

bool (Funcs (CPNT2,CPNT1)) is non empty set

bool CPNT2 is non empty set

[:{},CPNT1:] is empty trivial Relation-like non-empty empty-yielding Function-like one-to-one constant functional finite finite-yielding V32() set

bool [:{},CPNT1:] is non empty finite V32() set

the empty trivial non proper Relation-like non-empty empty-yielding {} -defined CPNT1 -valued Function-like one-to-one constant functional total quasi_total finite finite-yielding V32() Element of bool [:{},CPNT1:] is empty trivial non proper Relation-like non-empty empty-yielding {} -defined CPNT1 -valued Function-like one-to-one constant functional total quasi_total finite finite-yielding V32() Element of bool [:{},CPNT1:]

(CPNT1,CPNT2,{}, the empty trivial non proper Relation-like non-empty empty-yielding {} -defined CPNT1 -valued Function-like one-to-one constant functional total quasi_total finite finite-yielding V32() Element of bool [:{},CPNT1:]) is non empty functional Element of bool (Funcs (CPNT2,CPNT1))

CPNT1 is non empty set

CPNT2 is set

bool CPNT2 is non empty set

[:CPNT2,CPNT1:] is Relation-like set

bool [:CPNT2,CPNT1:] is non empty set

O is non empty functional (CPNT1,CPNT2)

q is Element of bool CPNT2

[:q,CPNT1:] is Relation-like set

bool [:q,CPNT1:] is non empty set

CA is Relation-like q -defined CPNT1 -valued Function-like total quasi_total Element of bool [:q,CPNT1:]

(CPNT1,CPNT2,q,CA) is non empty functional Element of bool (Funcs (CPNT2,CPNT1))

Funcs (CPNT2,CPNT1) is non empty functional FUNCTION_DOMAIN of CPNT2,CPNT1

bool (Funcs (CPNT2,CPNT1)) is non empty set

{ b

CPNT1 is non empty set

CPNT2 is non empty set

O is set

q is non empty functional (CPNT1,O)

bool O is non empty set

[:O,CPNT1:] is Relation-like set

bool [:O,CPNT1:] is non empty set

CA is Element of bool O

[:CA,CPNT1:] is Relation-like set

bool [:CA,CPNT1:] is non empty set

CB is Relation-like CA -defined CPNT1 -valued Function-like total quasi_total Element of bool [:CA,CPNT1:]

{ b

[:CA,CPNT2:] is Relation-like set

bool [:CA,CPNT2:] is non empty set

[:O,CPNT2:] is Relation-like set

bool [:O,CPNT2:] is non empty set

q12A is Relation-like CA -defined CPNT2 -valued Function-like total quasi_total Element of bool [:CA,CPNT2:]

{ b

O12A is set

O21A is Relation-like O -defined CPNT1 -valued Function-like total quasi_total Element of bool [:O,CPNT1:]

O21A | CA is Relation-like O -defined CA -defined O -defined CPNT1 -valued Function-like Element of bool [:O,CPNT1:]

q12B is Relation-like O -defined CPNT2 -valued Function-like total quasi_total Element of bool [:O,CPNT2:]

q12B | CA is Relation-like O -defined CA -defined O -defined CPNT2 -valued Function-like Element of bool [:O,CPNT2:]

(CPNT2,O,CA,q12A) is non empty functional Element of bool (Funcs (O,CPNT2))

Funcs (O,CPNT2) is non empty functional FUNCTION_DOMAIN of O,CPNT2

bool (Funcs (O,CPNT2)) is non empty set

O12A is non empty functional (CPNT2,O)

CPNT2 is set

CPNT1 is non empty set

Funcs (CPNT2,CPNT1) is non empty functional FUNCTION_DOMAIN of CPNT2,CPNT1

bool (Funcs (CPNT2,CPNT1)) is non empty set

{ b

bool (bool (Funcs (CPNT2,CPNT1))) is non empty set

the non empty functional (CPNT1,CPNT2) is non empty functional (CPNT1,CPNT2)

q is set

bool (Funcs (CPNT2,CPNT1)) is non empty Element of bool (bool (Funcs (CPNT2,CPNT1)))

CA is functional Element of bool (Funcs (CPNT2,CPNT1))

CPNT1 is non empty set

CPNT2 is set

O is set

(CPNT1,CPNT2) is non empty Element of bool (bool (Funcs (CPNT2,CPNT1)))

Funcs (CPNT2,CPNT1) is non empty functional FUNCTION_DOMAIN of CPNT2,CPNT1

bool (Funcs (CPNT2,CPNT1)) is non empty set

bool (bool (Funcs (CPNT2,CPNT1))) is non empty set

{ b

PFuncs (O,CPNT1) is non empty functional set

bool (PFuncs (O,CPNT1)) is non empty Element of bool (bool (PFuncs (O,CPNT1)))

bool (PFuncs (O,CPNT1)) is non empty set

bool (bool (PFuncs (O,CPNT1))) is non empty set

PFuncs (CPNT2,CPNT1) is non empty functional set

bool (Funcs (CPNT2,CPNT1)) is non empty Element of bool (bool (Funcs (CPNT2,CPNT1)))

q is set

CA is functional Element of bool (Funcs (CPNT2,CPNT1))

CPNT1 is non empty non trivial set

CPNT2 is set

bool CPNT2 is non empty set

[:CPNT2,CPNT1:] is Relation-like set

bool [:CPNT2,CPNT1:] is non empty set

O is Element of bool CPNT2

[:O,CPNT1:] is Relation-like set

bool [:O,CPNT1:] is non empty set

q is Element of bool CPNT2

[:q,CPNT1:] is Relation-like set

bool [:q,CPNT1:] is non empty set

CA is Relation-like O -defined CPNT1 -valued Function-like total quasi_total Element of bool [:O,CPNT1:]

CB is Relation-like q -defined CPNT1 -valued Function-like total quasi_total Element of bool [:q,CPNT1:]

q12A is set

dom CB is Element of bool q

bool q is non empty set

CB . q12A is set

q21A is set

O12A is set

q21A is set

q21A is set

O12A is set

CA . O12A is set

O12A is Relation-like CPNT2 -defined CPNT1 -valued Function-like total quasi_total Element of bool [:CPNT2,CPNT1:]

O21A is set

dom CA is Element of bool O

bool O is non empty set

CA . O21A is set

O12A . O21A is set

O12A . q12A is set

O12A | q is Relation-like CPNT2 -defined q -defined CPNT2 -defined CPNT1 -valued Function-like Element of bool [:CPNT2,CPNT1:]

CPNT2 /\ O is Element of bool CPNT2

dom O12A is Element of bool CPNT2

(dom O12A) /\ O is Element of bool CPNT2

O12A | O is Relation-like CPNT2 -defined O -defined CPNT2 -defined CPNT1 -valued Function-like Element of bool [:CPNT2,CPNT1:]

CPNT1 is non empty non trivial set

CPNT2 is set

bool CPNT2 is non empty set

[:CPNT2,CPNT1:] is Relation-like set

bool [:CPNT2,CPNT1:] is non empty set

O is Element of bool CPNT2

[:O,CPNT1:] is Relation-like set

bool [:O,CPNT1:] is non empty set

q is Element of bool CPNT2

[:q,CPNT1:] is Relation-like set

bool [:q,CPNT1:] is non empty set

CA is Relation-like O -defined CPNT1 -valued Function-like total quasi_total Element of bool [:O,CPNT1:]

CB is Relation-like q -defined CPNT1 -valued Function-like total quasi_total Element of bool [:q,CPNT1:]

q12A is set

dom CA is Element of bool O

bool O is non empty set

CA . q12A is set

q21A is set

O12A is set

q21A is set

q21A is set

O12A is set

CB . O12A is set

O12A is Relation-like CPNT2 -defined CPNT1 -valued Function-like total quasi_total Element of bool [:CPNT2,CPNT1:]

O21A is set

dom CB is Element of bool q

bool q is non empty set

CB . O21A is set

O12A . O21A is set

O12A . q12A is set

O12A | O is Relation-like CPNT2 -defined O -defined CPNT2 -defined CPNT1 -valued Function-like Element of bool [:CPNT2,CPNT1:]

CPNT2 /\ q is Element of bool CPNT2

dom O12A is Element of bool CPNT2

(dom O12A) /\ q is Element of bool CPNT2

O12A | q is Relation-like CPNT2 -defined q -defined CPNT2 -defined CPNT1 -valued Function-like Element of bool [:CPNT2,CPNT1:]

CPNT1 is non empty non trivial set

CPNT2 is set

bool CPNT2 is non empty set

[:CPNT2,CPNT1:] is Relation-like set

bool [:CPNT2,CPNT1:] is non empty set

O is Element of bool CPNT2

[:O,CPNT1:] is Relation-like set

bool [:O,CPNT1:] is non empty set

q is Element of bool CPNT2

[:q,CPNT1:] is Relation-like set

bool [:q,CPNT1:] is non empty set

CA is Relation-like O -defined CPNT1 -valued Function-like total quasi_total Element of bool [:O,CPNT1:]

{ b

CB is Relation-like q -defined CPNT1 -valued Function-like total quasi_total Element of bool [:q,CPNT1:]

{ b

q12A is Relation-like CPNT2 -defined CPNT1 -valued Function-like total quasi_total Element of bool [:CPNT2,CPNT1:]

q12A | O is Relation-like CPNT2 -defined O -defined CPNT2 -defined CPNT1 -valued Function-like Element of bool [:CPNT2,CPNT1:]

q12A | q is Relation-like CPNT2 -defined q -defined CPNT2 -defined CPNT1 -valued Function-like Element of bool [:CPNT2,CPNT1:]

q21A is Relation-like CPNT2 -defined CPNT1 -valued Function-like total quasi_total Element of bool [:CPNT2,CPNT1:]

q21A | q is Relation-like CPNT2 -defined q -defined CPNT2 -defined CPNT1 -valued Function-like Element of bool [:CPNT2,CPNT1:]

q12A is Relation-like CPNT2 -defined CPNT1 -valued Function-like total quasi_total Element of bool [:CPNT2,CPNT1:]

q12A | q is Relation-like CPNT2 -defined q -defined CPNT2 -defined CPNT1 -valued Function-like Element of bool [:CPNT2,CPNT1:]

q12A | O is Relation-like CPNT2 -defined O -defined CPNT2 -defined CPNT1 -valued Function-like Element of bool [:CPNT2,CPNT1:]

q21A is Relation-like CPNT2 -defined CPNT1 -valued Function-like total quasi_total Element of bool [:CPNT2,CPNT1:]

q21A | O is Relation-like CPNT2 -defined O -defined CPNT2 -defined CPNT1 -valued Function-like Element of bool [:CPNT2,CPNT1:]

CPNT1 is non empty non trivial set

CPNT2 is set

O is set

[:O,CPNT1:] is Relation-like set

bool [:O,CPNT1:] is non empty set

q is Relation-like O -defined CPNT1 -valued Function-like total quasi_total Element of bool [:O,CPNT1:]

(CPNT1,CPNT2,O,q) is non empty functional Element of bool (Funcs (CPNT2,CPNT1))

Funcs (CPNT2,CPNT1) is non empty functional FUNCTION_DOMAIN of CPNT2,CPNT1

bool (Funcs (CPNT2,CPNT1)) is non empty set

CA is set

[:CA,CPNT1:] is Relation-like set

bool [:CA,CPNT1:] is non empty set

CB is Relation-like CA -defined CPNT1 -valued Function-like total quasi_total Element of bool [:CA,CPNT1:]

(CPNT1,CPNT2,CA,CB) is non empty functional Element of bool (Funcs (CPNT2,CPNT1))

[:CPNT2,CPNT1:] is Relation-like set

bool [:CPNT2,CPNT1:] is non empty set

{ b

q12A is set

{ b

q21A is Relation-like CPNT2 -defined CPNT1 -valued Function-like total quasi_total Element of bool [:CPNT2,CPNT1:]

q21A | CA is Relation-like CPNT2 -defined CA -defined CPNT2 -defined CPNT1 -valued Function-like Element of bool [:CPNT2,CPNT1:]

O12A is Relation-like CPNT2 -defined CPNT1 -valued Function-like total quasi_total Element of bool [:CPNT2,CPNT1:]

O12A | O is Relation-like CPNT2 -defined O -defined CPNT2 -defined CPNT1 -valued Function-like Element of bool [:CPNT2,CPNT1:]

CPNT1 is non empty set

CPNT2 is non empty set

O is set

q is set

(CPNT1,O) is non empty Element of bool (bool (Funcs (O,CPNT1)))

Funcs (O,CPNT1) is non empty functional FUNCTION_DOMAIN of O,CPNT1

bool (Funcs (O,CPNT1)) is non empty set

bool (bool (Funcs (O,CPNT1))) is non empty set

{ b

(CPNT2,q) is non empty Element of bool (bool (Funcs (q,CPNT2)))

Funcs (q,CPNT2) is non empty functional FUNCTION_DOMAIN of q,CPNT2

bool (Funcs (q,CPNT2)) is non empty set

bool (bool (Funcs (q,CPNT2))) is non empty set

{ b

[:(CPNT1,O),(CPNT2,q):] is non empty Relation-like set

bool [:(CPNT1,O),(CPNT2,q):] is non empty set

bool O is non empty set

CA is set

q12A is functional Element of bool (Funcs (O,CPNT1))

CB is non empty functional (CPNT1,O)

q12A is Element of bool O

[:q12A,CPNT1:] is Relation-like set

bool [:q12A,CPNT1:] is non empty set

q21A is Relation-like q12A -defined CPNT1 -valued Function-like total quasi_total Element of bool [:q12A,CPNT1:]

(CPNT1,O,q12A,q21A) is non empty functional Element of bool (Funcs (O,CPNT1))

[:q12A,CPNT2:] is Relation-like set

bool [:q12A,CPNT2:] is non empty set

O12A is Relation-like q12A -defined CPNT2 -valued Function-like total quasi_total Element of bool [:q12A,CPNT2:]

(CPNT2,q,q12A,O12A) is non empty functional Element of bool (Funcs (q,CPNT2))

q12B is set

q21B is set

CA is non empty Relation-like (CPNT1,O) -defined (CPNT2,q) -valued Function-like total quasi_total Element of bool [:(CPNT1,O),(CPNT2,q):]

CB is set

CA . CB is set

CPNT2 is non empty set

CPNT1 is non empty set

q is set

(CPNT2,q) is non empty Element of bool (bool (Funcs (q,CPNT2)))

Funcs (q,CPNT2) is non empty functional FUNCTION_DOMAIN of q,CPNT2

bool (Funcs (q,CPNT2)) is non empty set

bool (bool (Funcs (q,CPNT2))) is non empty set

{ b

O is set

(CPNT1,O) is non empty Element of bool (bool (Funcs (O,CPNT1)))

Funcs (O,CPNT1) is non empty functional FUNCTION_DOMAIN of O,CPNT1

bool (Funcs (O,CPNT1)) is non empty set

bool (bool (Funcs (O,CPNT1))) is non empty set

{ b

[:(CPNT2,q),(CPNT1,O):] is non empty Relation-like set

bool [:(CPNT2,q),(CPNT1,O):] is non empty set

bool q is non empty set

bool O is non empty set

CA is set

q12A is functional Element of bool (Funcs (q,CPNT2))

CB is non empty functional (CPNT2,q)

q12A is Element of bool q

[:q12A,CPNT2:] is Relation-like set

bool [:q12A,CPNT2:] is non empty set

q21A is Relation-like q12A -defined CPNT2 -valued Function-like total quasi_total Element of bool [:q12A,CPNT2:]

(CPNT2,q,q12A,q21A) is non empty functional Element of bool (Funcs (q,CPNT2))

O /\ q12A is Element of bool q

q21A " CPNT1 is set

(O /\ q12A) /\ (q21A " CPNT1) is Element of bool q

q21A | ((O /\ q12A) /\ (q21A " CPNT1)) is Relation-like q12A -defined (O /\ q12A) /\ (q21A " CPNT1) -defined q12A -defined CPNT2 -valued Function-like Element of bool [:q12A,CPNT2:]

[:((O /\ q12A) /\ (q21A " CPNT1)),CPNT2:] is Relation-like set

bool [:((O /\ q12A) /\ (q21A " CPNT1)),CPNT2:] is non empty set

rng (q21A | ((O /\ q12A) /\ (q21A " CPNT1))) is set

q21A .: ((O /\ q12A) /\ (q21A " CPNT1)) is set

q21A .: (q21A " CPNT1) is set

[:((O /\ q12A) /\ (q21A " CPNT1)),CPNT1:] is Relation-like set

bool [:((O /\ q12A) /\ (q21A " CPNT1)),CPNT1:] is non empty set

q12B is Relation-like (O /\ q12A) /\ (q21A " CPNT1) -defined CPNT1 -valued Function-like total quasi_total Element of bool [:((O /\ q12A) /\ (q21A " CPNT1)),CPNT1:]

(CPNT1,O,((O /\ q12A) /\ (q21A " CPNT1)),q12B) is non empty functional Element of bool (Funcs (O,CPNT1))

O12B is set

O21B is set

CA is non empty Relation-like (CPNT2,q) -defined (CPNT1,O) -valued Function-like total quasi_total Element of bool [:(CPNT2,q),(CPNT1,O):]

CB is set

CA . CB is set

CPNT1 is non empty non trivial set

CPNT2 is non empty non trivial set

O is set

q is set

(CPNT1,O) is non empty Element of bool (bool (Funcs (O,CPNT1)))

Funcs (O,CPNT1) is non empty functional FUNCTION_DOMAIN of O,CPNT1

bool (Funcs (O,CPNT1)) is non empty set

bool (bool (Funcs (O,CPNT1))) is non empty set

{ b

(CPNT2,q) is non empty Element of bool (bool (Funcs (q,CPNT2)))

Funcs (q,CPNT2) is non empty functional FUNCTION_DOMAIN of q,CPNT2

bool (Funcs (q,CPNT2)) is non empty set

bool (bool (Funcs (q,CPNT2))) is non empty set

{ b

[:(CPNT1,O),(CPNT2,q):] is non empty Relation-like set

bool [:(CPNT1,O),(CPNT2,q):] is non empty set

bool O is non empty set

CA is non empty Relation-like (CPNT1,O) -defined (CPNT2,q) -valued Function-like total quasi_total Element of bool [:(CPNT1,O),(CPNT2,q):]

CB is non empty Relation-like (CPNT1,O) -defined (CPNT2,q) -valued Function-like total quasi_total Element of bool [:(CPNT1,O),(CPNT2,q):]

q12A is set

CA . q12A is set

q21A is Element of bool O

[:q21A,CPNT1:] is Relation-like set

bool [:q21A,CPNT1:] is non empty set

[:q21A,CPNT2:] is Relation-like set

bool [:q21A,CPNT2:] is non empty set

O12A is Relation-like q21A -defined CPNT1 -valued Function-like total quasi_total Element of bool [:q21A,CPNT1:]

O21A is Relation-like q21A -defined CPNT2 -valued Function-like total quasi_total Element of bool [:q21A,CPNT2:]

(CPNT1,O,q21A,O12A) is non empty functional Element of bool (Funcs (O,CPNT1))

(CPNT2,q,q21A,O21A) is non empty functional Element of bool (Funcs (q,CPNT2))

CB . q12A is set

q12B is Element of bool O

[:q12B,CPNT1:] is Relation-like set

bool [:q12B,CPNT1:] is non empty set

[:q12B,CPNT2:] is Relation-like set

bool [:q12B,CPNT2:] is non empty set

q21B is Relation-like q12B -defined CPNT1 -valued Function-like total quasi_total Element of bool [:q12B,CPNT1:]

O12B is Relation-like q12B -defined CPNT2 -valued Function-like total quasi_total Element of bool [:q12B,CPNT2:]

(CPNT1,O,q12B,q21B) is non empty functional Element of bool (Funcs (O,CPNT1))

(CPNT2,q,q12B,O12B) is non empty functional Element of bool (Funcs (q,CPNT2))

CPNT2 is non empty non trivial set

q is set

(CPNT2,q) is non empty Element of bool (bool (Funcs (q,CPNT2)))

Funcs (q,CPNT2) is non empty functional FUNCTION_DOMAIN of q,CPNT2

bool (Funcs (q,CPNT2)) is non empty set

bool (bool (Funcs (q,CPNT2))) is non empty set

{ b

CPNT1 is non empty set

O is set

(CPNT1,O) is non empty Element of bool (bool (Funcs (O,CPNT1)))

Funcs (O,CPNT1) is non empty functional FUNCTION_DOMAIN of O,CPNT1

bool (Funcs (O,CPNT1)) is non empty set

bool (bool (Funcs (O,CPNT1))) is non empty set

{ b

[:(CPNT2,q),(CPNT1,O):] is non empty Relation-like set

bool [:(CPNT2,q),(CPNT1,O):] is non empty set

bool q is non empty set

bool O is non empty set

CA is non empty Relation-like (CPNT2,q) -defined (CPNT1,O) -valued Function-like total quasi_total Element of bool [:(CPNT2,q),(CPNT1,O):]

CB is non empty Relation-like (CPNT2,q) -defined (CPNT1,O) -valued Function-like total quasi_total Element of bool [:(CPNT2,q),(CPNT1,O):]

q12A is set

CA . q12A is set

O12A is Element of bool O

[:O12A,CPNT1:] is Relation-like set

bool [:O12A,CPNT1:] is non empty set

q21A is Element of bool q

[:q21A,CPNT2:] is Relation-like set

bool [:q21A,CPNT2:] is non empty set

O /\ q21A is Element of bool q

q12B is Relation-like q21A -defined CPNT2 -valued Function-like total quasi_total Element of bool [:q21A,CPNT2:]

q12B " CPNT1 is set

(O /\ q21A) /\ (q12B " CPNT1) is Element of bool q

O21A is Relation-like O12A -defined CPNT1 -valued Function-like total quasi_total Element of bool [:O12A,CPNT1:]

q12B | O12A is Relation-like O12A -defined q21A -defined CPNT2 -valued Function-like Element of bool [:q21A,CPNT2:]

(CPNT2,q,q21A,q12B) is non empty functional Element of bool (Funcs (q,CPNT2))

(CPNT1,O,O12A,O21A) is non empty functional Element of bool (Funcs (O,CPNT1))

CB . q12A is set

O12B is Element of bool O

[:O12B,CPNT1:] is Relation-like set

bool [:O12B,CPNT1:] is non empty set

q21B is Element of bool q

[:q21B,CPNT2:] is Relation-like set

bool [:q21B,CPNT2:] is non empty set

O /\ q21B is Element of bool q

TTS12 is Relation-like q21B -defined CPNT2 -valued Function-like total quasi_total Element of bool [:q21B,CPNT2:]

TTS12 " CPNT1 is set

(O /\ q21B) /\ (TTS12 " CPNT1) is Element of bool q

O21B is Relation-like O12B -defined CPNT1 -valued Function-like total quasi_total Element of bool [:O12B,CPNT1:]

TTS12 | O12B is Relation-like O12B -defined q21B -defined CPNT2 -valued Function-like Element of bool [:q21B,CPNT2:]

(CPNT2,q,q21B,TTS12) is non empty functional Element of bool (Funcs (q,CPNT2))

(CPNT1,O,O12B,O21B) is non empty functional Element of bool (Funcs (O,CPNT1))

CPNT1 is non empty non trivial set

CPNT2 is set

bool CPNT2 is non empty set

O is non empty functional (CPNT1,CPNT2)

[:CPNT2,CPNT1:] is Relation-like set

bool [:CPNT2,CPNT1:] is non empty set

q is Element of bool CPNT2

[:q,CPNT1:] is Relation-like set

bool [:q,CPNT1:] is non empty set

CA is Relation-like q -defined CPNT1 -valued Function-like total quasi_total Element of bool [:q,CPNT1:]

{ b

CB is Element of bool CPNT2

[:CB,CPNT1:] is Relation-like set

bool [:CB,CPNT1:] is non empty set

q21A is Element of bool CPNT2

[:q21A,CPNT1:] is Relation-like set

bool [:q21A,CPNT1:] is non empty set

q12A is Relation-like CB -defined CPNT1 -valued Function-like total quasi_total Element of bool [:CB,CPNT1:]

{ b

q is finite Element of bool CPNT2

O12A is Relation-like q21A -defined CPNT1 -valued Function-like total quasi_total Element of bool [:q21A,CPNT1:]

{ b

CA is finite Element of bool CPNT2

CPNT1 is non empty non trivial set

O is set

(CPNT1,O) is non empty Element of bool (bool (Funcs (O,CPNT1)))

Funcs (O,CPNT1) is non empty functional FUNCTION_DOMAIN of O,CPNT1

bool (Funcs (O,CPNT1)) is non empty set

bool (bool (Funcs (O,CPNT1))) is non empty set

{ b

CA is non empty non trivial set

q12A is set

(CA,q12A) is non empty Element of bool (bool (Funcs (q12A,CA)))

Funcs (q12A,CA) is non empty functional FUNCTION_DOMAIN of q12A,CA

bool (Funcs (q12A,CA)) is non empty set

bool (bool (Funcs (q12A,CA))) is non empty set

{ b

[:(CPNT1,O),(CA,q12A):] is non empty Relation-like set

bool [:(CPNT1,O),(CA,q12A):] is non empty set

CPNT2 is non empty non trivial set

q is set

(CPNT2,q) is non empty Element of bool (bool (Funcs (q,CPNT2)))

Funcs (q,CPNT2) is non empty functional FUNCTION_DOMAIN of q,CPNT2

bool (Funcs (q,CPNT2)) is non empty set

bool (bool (Funcs (q,CPNT2))) is non empty set

{ b

CB is non empty non trivial set

q21A is set

(CB,q21A) is non empty Element of bool (bool (Funcs (q21A,CB)))

Funcs (q21A,CB) is non empty functional FUNCTION_DOMAIN of q21A,CB

bool (Funcs (q21A,CB)) is non empty set

bool (bool (Funcs (q21A,CB))) is non empty set

{ b

(CPNT1,CPNT2,O,q) is non empty Relation-like (CPNT2,q) -defined (CPNT1,O) -valued Function-like total quasi_total Element of bool [:(CPNT2,q),(CPNT1,O):]

[:(CPNT2,q),(CPNT1,O):] is non empty Relation-like set

bool [:(CPNT2,q),(CPNT1,O):] is non empty set

O12A is non empty Relation-like (CPNT1,O) -defined (CA,q12A) -valued Function-like total quasi_total Element of bool [:(CPNT1,O),(CA,q12A):]

(CA,CB,q12A,q21A) is non empty Relation-like (CA,q12A) -defined (CB,q21A) -valued Function-like total quasi_total Element of bool [:(CA,q12A),(CB,q21A):]

[:(CA,q12A),(CB,q21A):] is non empty Relation-like set

bool [:(CA,q12A),(CB,q21A):] is non empty set

(CA,CB,q12A,q21A) * O12A is non empty Relation-like (CPNT1,O) -defined (CB,q21A) -valued Function-like total quasi_total Element of bool [:(CPNT1,O),(CB,q21A):]

[:(CPNT1,O),(CB,q21A):] is non empty Relation-like set

bool [:(CPNT1,O),(CB,q21A):] is non empty set

((CA,CB,q12A,q21A) * O12A) * (CPNT1,CPNT2,O,q) is non empty Relation-like (CPNT2,q) -defined (CB,q21A) -valued Function-like total quasi_total Element of bool [:(CPNT2,q),(CB,q21A):]

[:(CPNT2,q),(CB,q21A):] is non empty Relation-like set

bool [:(CPNT2,q),(CB,q21A):] is non empty set

{{}} is non empty trivial functional finite V32() set

[#] ({{}},{{}}) is non empty Relation-like {{}} -defined {{}} -valued finite Element of bool [:{{}},{{}}:]

[:{{}},{{}}:] is non empty Relation-like finite set

bool [:{{}},{{}}:] is non empty finite V32() set

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

() is ()

the S-T_Arcs of () is Relation-like the carrier of () -defined the carrier' of () -valued Element of bool [: the carrier of (), the carrier' of ():]

the carrier of () is set

the carrier' of () is set

[: the carrier of (), the carrier' of ():] is Relation-like set

bool [: the carrier of (), the carrier' of ():] is non empty set

the T-S_Arcs of () is Relation-like the carrier' of () -defined the carrier of () -valued Element of bool [: the carrier' of (), the carrier of ():]

[: the carrier' of (), the carrier of ():] is Relation-like set

bool [: the carrier' of (), the carrier of ():] is non empty set

CPNT1 is non empty non void V49() with_S-T_arc with_T-S_arc ()

the carrier' of CPNT1 is non empty set

CPNT1 is non empty non void V49() with_S-T_arc with_T-S_arc ()

the carrier' of CPNT1 is non empty set

{ b

bool the carrier' of CPNT1 is non empty set

CPNT2 is set

O is Element of the carrier' of CPNT1

CPNT1 is non empty non void V49() with_S-T_arc with_T-S_arc ()

the carrier' of CPNT1 is non empty set

CPNT2 is Element of the carrier' of CPNT1

the of CPNT1 is Relation-like Function-like set

dom the of CPNT1 is set

the of CPNT1 is non empty finite set

bool the of CPNT1 is non empty finite V32() set

{CPNT2} is non empty trivial finite Element of bool the carrier' of CPNT1

bool the carrier' of CPNT1 is non empty set

*' {CPNT2} is Element of bool the carrier of CPNT1

the carrier of CPNT1 is non empty set

bool the carrier of CPNT1 is non empty set

the S-T_Arcs of CPNT1 is non empty Relation-like the carrier of CPNT1 -defined the carrier' of CPNT1 -valued Element of bool [: the carrier of CPNT1, the carrier' of CPNT1:]

[: the carrier of CPNT1, the carrier' of CPNT1:] is non empty Relation-like set

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

{ b

( b

bool (*' {CPNT2}) is non empty set

{CPNT2} *' is Element of bool the carrier of CPNT1

the T-S_Arcs of CPNT1 is non empty Relation-like the carrier' of CPNT1 -defined the carrier of CPNT1 -valued Element of bool [: the carrier' of CPNT1, the carrier of CPNT1:]

[: the carrier' of CPNT1, the carrier of CPNT1:] is non empty Relation-like set

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

{ b

( b

bool ({CPNT2} *') is non empty set

the of CPNT1 . CPNT2 is set

CPNT1 is non empty non void V49() with_S-T_arc with_T-S_arc ()

the carrier' of CPNT1 is non empty set

CPNT2 is non empty non void V49() with_S-T_arc with_T-S_arc ()

the carrier' of CPNT2 is non empty set

the carrier of CPNT1 is non empty set

the carrier of CPNT2 is non empty set

the S-T_Arcs of CPNT1 is non empty Relation-like the carrier of CPNT1 -defined the carrier' of CPNT1 -valued Element of bool [: the carrier of CPNT1, the carrier' of CPNT1:]

[: the carrier of CPNT1, the carrier' of CPNT1:] is non empty Relation-like set

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

the S-T_Arcs of CPNT2 is non empty Relation-like the carrier of CPNT2 -defined the carrier' of CPNT2 -valued Element of bool [: the carrier of CPNT2, the carrier' of CPNT2:]

[: the carrier of CPNT2, the carrier' of CPNT2:] is non empty Relation-like set

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

the T-S_Arcs of CPNT1 is non empty Relation-like the carrier' of CPNT1 -defined the carrier of CPNT1 -valued Element of bool [: the carrier' of CPNT1, the carrier of CPNT1:]

[: the carrier' of CPNT1, the carrier of CPNT1:] is non empty Relation-like set

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

the T-S_Arcs of CPNT2 is non empty Relation-like the carrier' of CPNT2 -defined the carrier of CPNT2 -valued Element of bool [: the carrier' of CPNT2, the carrier of CPNT2:]

[: the carrier' of CPNT2, the carrier of CPNT2:] is non empty Relation-like set

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

O is Element of the carrier' of CPNT1

{O} is non empty trivial finite Element of bool the carrier' of CPNT1

bool the carrier' of CPNT1 is non empty set

*' {O} is Element of bool the carrier of CPNT1

bool the carrier of CPNT1 is non empty set

{ b

( b

{O} *' is Element of bool the carrier of CPNT1

{ b

( b

q is Element of the carrier' of CPNT2

{q} is non empty trivial finite Element of bool the carrier' of CPNT2

bool the carrier' of CPNT2 is non empty set

*' {q} is Element of bool the carrier of CPNT2

bool the carrier of CPNT2 is non empty set

{ b

( b

{q} *' is Element of bool the carrier of CPNT2

{ b

( b

CA is set

CB is Element of the carrier of CPNT1

q21A is Element of the carrier' of CPNT1

q12A is Element of the S-T_Arcs of CPNT1

[CB,q21A] is non empty Element of [: the carrier of CPNT1, the carrier' of CPNT1:]

{CB,q21A} is non empty finite set

{CB} is non empty trivial finite set

{{CB,q21A},{CB}} is non empty finite V32() set

q12A is Element of the carrier' of CPNT1

CB is Element of the S-T_Arcs of CPNT1

[CA,q12A] is non empty set

{CA,q12A} is non empty finite set

{CA} is non empty trivial finite set

{{CA,q12A},{CA}} is non empty finite V32() set

CA is set

CB is Element of the carrier of CPNT1

q21A is Element of the carrier' of CPNT1

q12A is Element of the T-S_Arcs of CPNT1

[q21A,CB] is non empty Element of [: the carrier' of CPNT1, the carrier of CPNT1:]

{q21A,CB} is non empty finite set

{q21A} is non empty trivial finite set

{{q21A,CB},{q21A}} is non empty finite V32() set

q12A is Element of the carrier' of CPNT1

CB is Element of the T-S_Arcs of CPNT1

[q12A,CA] is non empty set

{q12A,CA} is non empty finite set

{q12A} is non empty trivial finite set

{{q12A,CA},{q12A}} is non empty finite V32() set

CPNT1 is Relation-like Function-like set

dom CPNT1 is set

CPNT2 is Relation-like Function-like set

dom CPNT2 is set

(dom CPNT1) /\ (dom CPNT2) is set

O is Relation-like Function-like set

dom O is set

(dom CPNT1) /\ (dom O) is set

q is Relation-like Function-like set

dom q is set

(dom CPNT1) /\ (dom q) is set

(dom CPNT2) /\ (dom O) is set

(dom CPNT2) /\ (dom q) is set

(dom O) /\ (dom q) is set

CA is Relation-like Function-like set

CPNT1 +* CPNT2 is Relation-like Function-like set

(CPNT1 +* CPNT2) +* O is Relation-like Function-like set

((CPNT1 +* CPNT2) +* O) +* q is Relation-like Function-like set

q21A is set

CA . q21A is set

CPNT1 . q21A is set

((CPNT1 +* CPNT2) +* O) . q21A is set

(CPNT1 +* CPNT2) . q21A is set

q21A is set

CA . q21A is set

CPNT2 . q21A is set

((CPNT1 +* CPNT2) +* O) . q21A is set

(CPNT1 +* CPNT2) . q21A is set

q21A is set

CA . q21A is set

O . q21A is set

((CPNT1 +* CPNT2) +* O) . q21A is set

q21A is set

CA . q21A is set

q . q21A is set

CPNT1 is set

CPNT2 is set

CPNT1 /\ CPNT2 is set

O is set

q is set

CA is set

CPNT1 \ O is Element of bool CPNT1

bool CPNT1 is non empty set

CB is set

CPNT2 \ q is Element of bool CPNT2

bool CPNT2 is non empty set

q12A is set

q21A is set

CA /\ CB is set

CA /\ q12A is set

CA /\ q21A is set

CB /\ q12A is set

CB /\ q21A is set

q12A /\ q21A is set

(CPNT1 \ O) /\ (CPNT2 \ q) is Element of bool CPNT2

O /\ CPNT1 is set

(CPNT1 \ O) /\ O is Element of bool CPNT1

(O /\ CPNT1) \ O is Element of bool (O /\ CPNT1)

bool (O /\ CPNT1) is non empty set

(CPNT1 \ O) /\ q is Element of bool CPNT1

(CPNT2 \ q) /\ O is Element of bool CPNT2

CPNT2 /\ q is set

(CPNT2 \ q) /\ q is Element of bool CPNT2

(CPNT2 /\ q) \ q is Element of bool (CPNT2 /\ q)

bool (CPNT2 /\ q) is non empty set

the set is set

{ the set } is non empty trivial finite set

[:{ the set },{{}}:] is non empty Relation-like finite set

bool [:{ the set },{{}}:] is non empty finite V32() set

[:{{}},{ the set }:] is non empty Relation-like finite set

bool [:{{}},{ the set }:] is non empty finite V32() set

{ the set , the set , the set } is non empty finite set

({ the set , the set , the set },{{}}) is non empty Element of bool (bool (Funcs ({{}},{ the set , the set , the set })))

Funcs ({{}},{ the set , the set , the set }) is non empty functional FUNCTION_DOMAIN of {{}},{ the set , the set , the set }

bool (Funcs ({{}},{ the set , the set , the set })) is non empty set

bool (bool (Funcs ({{}},{ the set , the set , the set }))) is non empty set

{ b

[:({ the set , the set , the set },{{}}),({ the set , the set , the set },{{}}):] is non empty Relation-like set

bool [:({ the set , the set , the set },{{}}),({ the set , the set , the set },{{}}):] is non empty set

the non empty Relation-like ({ the set , the set , the set },{{}}) -defined ({ the set , the set , the set },{{}}) -valued Function-like total quasi_total Element of bool [:({ the set , the set , the set },{{}}),({ the set , the set , the set },{{}}):] is non empty Relation-like ({ the set , the set , the set },{{}}) -defined ({ the set , the set , the set },{{}}) -valued Function-like total quasi_total Element of bool [:({ the set , the set , the set },{{}}),({ the set , the set , the set },{{}}):]

{ the set } --> the non empty Relation-like ({ the set , the set , the set },{{}}) -defined ({ the set , the set , the set },{{}}) -valued Function-like total quasi_total Element of bool [:({ the set , the set , the set },{{}}),({ the set , the set , the set },{{}}):] is non empty Relation-like { the set } -defined bool [:({ the set , the set , the set },{{}}),({ the set , the set , the set },{{}}):] -valued Function-like total quasi_total finite Element of bool [:{ the set },(bool [:({ the set , the set , the set },{{}}),({ the set , the set , the set },{{}}):]):]

[:{ the set },(bool [:({ the set , the set , the set },{{}}),({ the set , the set , the set },{{}}):]):] is non empty Relation-like set

bool [:{ the set },(bool [:({ the set , the set , the set },{{}}),({ the set , the set , the set },{{}}):]):] is non empty set

q12A is non empty Relation-like {{}} -defined { the set } -valued finite Element of bool [:{{}},{ the set }:]

CA is non empty Relation-like { the set } -defined {{}} -valued finite Element of bool [:{ the set },{{}}:]

({{}},{ the set },q12A,CA,{ the set , the set , the set },({ the set } --> the non empty Relation-like ({ the set , the set , the set },{{}}) -defined ({ the set , the set , the set },{{}}) -valued Function-like total quasi_total Element of bool [:({ the set , the set , the set },{{}}),({ the set , the set , the set },{{}}):])) is () ()

q21B is non empty non void V49() with_S-T_arc with_T-S_arc ()

the of q21B is non empty finite set

bool the of q21B is non empty finite V32() set

the carrier' of q21B is non empty set

O21B is Element of the carrier' of q21B

the of q21B is Relation-like Function-like set

dom the of q21B is set

[ the set ,{}] is non empty set

{ the set ,{}} is non empty finite set

{{ the set ,{}},{ the set }} is non empty finite V32() set

{O21B} is non empty trivial finite Element of bool the carrier' of q21B

bool the carrier' of q21B is non empty set

{O21B} *' is Element of bool the carrier of q21B

the carrier of q21B is non empty set

bool the carrier of q21B is non empty set

the T-S_Arcs of q21B is non empty Relation-like the carrier' of q21B -defined the carrier of q21B -valued Element of bool [: the carrier' of q21B, the carrier of q21B:]

[: the carrier' of q21B, the carrier of q21B:] is non empty Relation-like set

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

{ b

( b

bool ({O21B} *') is non empty set

[{}, the set ] is non empty set

{{}, the set } is non empty finite set

{{{}, the set },{{}}} is non empty finite V32() set

*' {O21B} is Element of bool the carrier of q21B

the S-T_Arcs of q21B is non empty Relation-like the carrier of q21B -defined the carrier' of q21B -valued Element of bool [: the carrier of q21B, the carrier' of q21B:]

[: the carrier of q21B, the carrier' of q21B:] is non empty Relation-like set

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

{ b

( b

bool (*' {O21B}) is non empty set

O12B is non empty finite Element of bool the of q21B

q12 is Element of bool (*' {O21B})

(O12B,q12) is non empty Element of bool (bool (Funcs (q12,O12B)))

Funcs (q12,O12B) is non empty functional FUNCTION_DOMAIN of q12,O12B

bool (Funcs (q12,O12B)) is non empty set

bool (bool (Funcs (q12,O12B))) is non empty set

{ b

TTS12 is Element of bool ({O21B} *')

(O12B,TTS12) is non empty Element of bool (bool (Funcs (TTS12,O12B)))

Funcs (TTS12,O12B) is non empty functional FUNCTION_DOMAIN of TTS12,O12B

bool (Funcs (TTS12,O12B)) is non empty set

bool (bool (Funcs (TTS12,O12B))) is non empty set

{ b

[:(O12B,q12),(O12B,TTS12):] is non empty Relation-like set

bool [:(O12B,q12),(O12B,TTS12):] is non empty set

({ the set } --> the non empty Relation-like ({ the set , the set , the set },{{}}) -defined ({ the set , the set , the set },{{}}) -valued Function-like total quasi_total Element of bool [:({ the set , the set , the set },{{}}),({ the set , the set , the set },{{}}):]) . O21B is set

the of q21B . O21B is set

dom ({ the set } --> the non empty Relation-like ({ the set , the set , the set },{{}}) -defined ({ the set , the set , the set },{{}}) -valued Function-like total quasi_total Element of bool [:({ the set , the set , the set },{{}}),({ the set , the set , the set },{{}}):]) is non empty trivial finite Element of bool { the set }

bool { the set } is non empty finite V32() set

O12B is Element of the carrier' of q21B

[O12B,{}] is non empty set

{O12B,{}} is non empty finite set

{O12B} is non empty trivial finite set

{{O12B,{}},{O12B}} is non empty finite V32() set

{O12B} is non empty trivial finite Element of bool the carrier' of q21B

{O12B} *' is Element of bool the carrier of q21B

{ b

( b

(q21B) is Element of bool the carrier' of q21B

{ b

TTS12 is Element of the carrier' of q21B

O21B is set

the carrier' of q21B \ (q21B) is Element of bool the carrier' of q21B

O is non empty non void V49() with_S-T_arc with_T-S_arc ()

the carrier of O is non empty set

q is non empty non void V49() with_S-T_arc with_T-S_arc ()

the carrier of q is non empty set

the carrier of O /\ the carrier of q is set

the carrier' of O is non empty set

the carrier' of q is non empty set

the carrier' of O /\ the carrier' of q is set

the carrier of q /\ the carrier of O is set

the carrier' of q /\ the carrier' of O is set

CPNT1 is non empty non void V49() with_S-T_arc with_T-S_arc ()

(CPNT1) is Element of bool the carrier' of CPNT1

the carrier' of CPNT1 is non empty set

bool the carrier' of CPNT1 is non empty set

{ b

CPNT2 is non empty non void V49() with_S-T_arc with_T-S_arc ()

the carrier of CPNT2 is non empty set

[:(CPNT1), the carrier of CPNT2:] is Relation-like set

bool [:(CPNT1), the carrier of CPNT2:] is non empty set

(CPNT2) is Element of bool the carrier' of CPNT2

the carrier' of CPNT2 is non empty set

bool the carrier' of CPNT2 is non empty set

{ b

the carrier of CPNT1 is non empty set

[:(CPNT2), the carrier of CPNT1:] is Relation-like set

bool [:(CPNT2), the carrier of CPNT1:] is non empty set

the Relation-like (CPNT1) -defined the carrier of CPNT2 -valued Function-like total quasi_total Element of bool [:(CPNT1), the carrier of CPNT2:] is Relation-like (CPNT1) -defined the carrier of CPNT2 -valued Function-like total quasi_total Element of bool [:(CPNT1), the carrier of CPNT2:]

the Relation-like (CPNT2) -defined the carrier of CPNT1 -valued Function-like total quasi_total Element of bool [:(CPNT2), the carrier of CPNT1:] is Relation-like (CPNT2) -defined the carrier of CPNT1 -valued Function-like total quasi_total Element of bool [:(CPNT2), the carrier of CPNT1:]

[ the Relation-like (CPNT1) -defined the carrier of CPNT2 -valued Function-like total quasi_total Element of bool [:(CPNT1), the carrier of CPNT2:], the Relation-like (CPNT2) -defined the carrier of CPNT1 -valued Function-like total quasi_total Element of bool [:(CPNT2), the carrier of CPNT1:]] is non empty Element of [:(bool [:(CPNT1), the carrier of CPNT2:]),(bool [:(CPNT2), the carrier of CPNT1:]):]

[:(bool [:(CPNT1), the carrier of CPNT2:]),(bool [:(CPNT2), the carrier of CPNT1:]):] is non empty Relation-like set

{ the Relation-like (CPNT1) -defined the carrier of CPNT2 -valued Function-like total quasi_total Element of bool [:(CPNT1), the carrier of CPNT2:], the Relation-like (CPNT2) -defined the carrier of CPNT1 -valued Function-like total quasi_total Element of bool [:(CPNT2), the carrier of CPNT1:]} is non empty functional finite set

{ the Relation-like (CPNT1) -defined the carrier of CPNT2 -valued Function-like total quasi_total Element of bool [:(CPNT1), the carrier of CPNT2:]} is non empty trivial functional finite set

{{ the Relation-like (CPNT1) -defined the carrier of CPNT2 -valued Function-like total quasi_total Element of bool [:(CPNT1), the carrier of CPNT2:], the Relation-like (CPNT2) -defined the carrier of CPNT1 -valued Function-like total quasi_total Element of bool [:(CPNT2), the carrier of CPNT1:]},{ the Relation-like (CPNT1) -defined the carrier of CPNT2 -valued Function-like total quasi_total Element of bool [:(CPNT1), the carrier of CPNT2:]}} is non empty finite V32() set

CPNT1 is non empty non void V49() with_S-T_arc with_T-S_arc () ()

CPNT2 is non empty non void V49() with_S-T_arc with_T-S_arc () ()

(CPNT1) is Element of bool the carrier' of CPNT1

the carrier' of CPNT1 is non empty set

bool the carrier' of CPNT1 is non empty set

{ b

the carrier of CPNT2 is non empty set

[:(CPNT1), the carrier of CPNT2:] is Relation-like set

bool [:(CPNT1), the carrier of CPNT2:] is non empty set

(CPNT2) is Element of bool the carrier' of CPNT2

the carrier' of CPNT2 is non empty set

bool the carrier' of CPNT2 is non empty set

{ b

the carrier of CPNT1 is non empty set

[:(CPNT2), the carrier of CPNT1:] is Relation-like set

bool [:(CPNT2), the carrier of CPNT1:] is non empty set

O is (CPNT1,CPNT2)

the of CPNT1 is non empty finite set

the of CPNT2 is non empty finite set

PFuncs ( the carrier of CPNT1, the of CPNT2) is non empty functional set

bool (PFuncs ( the carrier of CPNT1, the of CPNT2)) is non empty Element of bool (bool (PFuncs ( the carrier of CPNT1, the of CPNT2)))

bool (PFuncs ( the carrier of CPNT1, the of CPNT2)) is non empty set

bool (bool (PFuncs ( the carrier of CPNT1, the of CPNT2))) is non empty set

PFuncs ( the carrier of CPNT2, the of CPNT2) is non empty functional set

bool (PFuncs ( the carrier of CPNT2, the of CPNT2)) is non empty Element of bool (bool (PFuncs ( the carrier of CPNT2, the of CPNT2)))

bool (PFuncs ( the carrier of CPNT2, the of CPNT2)) is non empty set

bool (bool (PFuncs ( the carrier of CPNT2, the of CPNT2))) is non empty set

PFuncs ( the carrier of CPNT2, the of CPNT1) is non empty functional set

bool (PFuncs ( the carrier of CPNT2, the of CPNT1)) is non empty Element of bool (bool (PFuncs ( the carrier of CPNT2, the of CPNT1)))

bool (PFuncs ( the carrier of CPNT2, the of CPNT1)) is non empty set

bool (bool (PFuncs ( the carrier of CPNT2, the of CPNT1))) is non empty set

PFuncs ( the carrier of CPNT1, the of CPNT1) is non empty functional set

bool (PFuncs ( the carrier of CPNT1, the of CPNT1)) is non empty Element of bool (bool (PFuncs ( the carrier of CPNT1, the of CPNT1)))

bool (PFuncs ( the carrier of CPNT1, the of CPNT1)) is non empty set

bool (bool (PFuncs ( the carrier of CPNT1, the of CPNT1))) is non empty set

PFuncs ((bool (PFuncs ( the carrier of CPNT1, the of CPNT1))),(bool (PFuncs ( the carrier of CPNT2, the of CPNT1)))) is non empty functional set

PFuncs ((bool (PFuncs ( the carrier of CPNT2, the of CPNT2))),(bool (PFuncs ( the carrier of CPNT1, the of CPNT2)))) is non empty functional set

q21B is Relation-like (CPNT1) -defined the carrier of CPNT2 -valued Function-like total quasi_total Element of bool [:(CPNT1), the carrier of CPNT2:]

O12B is Relation-like (CPNT2) -defined the carrier of CPNT1 -valued Function-like total quasi_total Element of bool [:(CPNT2), the carrier of CPNT1:]

[q21B,O12B] is non empty Element of [:(bool [:(CPNT1), the carrier of CPNT2:]),(bool [:(CPNT2), the carrier of CPNT1:]):]

[:(bool [:(CPNT1), the carrier of CPNT2:]),(bool [:(CPNT2), the carrier of CPNT1:]):] is non empty Relation-like set

{q21B,O12B} is non empty functional finite set

{q21B} is non empty trivial functional finite set

{{q21B,O12B},{q21B}} is non empty finite V32() set

O21B is set

TTS12 is Element of the carrier' of CPNT1

Im (q21B,TTS12) is Element of bool the carrier of CPNT2

bool the carrier of CPNT2 is non empty set

{TTS12} is non empty trivial finite Element of bool the carrier' of CPNT1

*' {TTS12} is Element of bool the carrier of CPNT1

bool the carrier of CPNT1 is non empty set

the S-T_Arcs of CPNT1 is non empty Relation-like the carrier of CPNT1 -defined the carrier' of CPNT1 -valued Element of bool [: the carrier of CPNT1, the carrier' of CPNT1:]

[: the carrier of CPNT1, the carrier' of CPNT1:] is non empty Relation-like set

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

{ b

( b

( the of CPNT1,(*' {TTS12})) is non empty Element of bool (bool (Funcs ((*' {TTS12}), the of CPNT1)))

Funcs ((*' {TTS12}), the of CPNT1) is non empty functional FUNCTION_DOMAIN of *' {TTS12}, the of CPNT1

bool (Funcs ((*' {TTS12}), the of CPNT1)) is non empty set

bool (bool (Funcs ((*' {TTS12}), the of CPNT1))) is non empty set

{ b

( the of CPNT1,(Im (q21B,TTS12))) is non empty Element of bool (bool (Funcs ((Im (q21B,TTS12)), the of CPNT1)))

Funcs ((Im (q21B,TTS12)), the of CPNT1) is non empty functional FUNCTION_DOMAIN of Im (q21B,TTS12), the of CPNT1

bool (Funcs ((Im (q21B,TTS12)), the of CPNT1)) is non empty set

bool (bool (Funcs ((Im (q21B,TTS12)), the of CPNT1))) is non empty set

{ b

[:( the of CPNT1,(*' {TTS12})),( the of CPNT1,(Im (q21B,TTS12))):] is non empty Relation-like set

bool [:( the of CPNT1,(*' {TTS12})),( the of CPNT1,(Im (q21B,TTS12))):] is non empty set

the non empty Relation-like ( the of CPNT1,(*' {TTS12})) -defined ( the of CPNT1,(Im (q21B,TTS12))) -valued Function-like total quasi_total Element of bool [:( the of CPNT1,(*' {TTS12})),( the of CPNT1,(Im (q21B,TTS12))):] is non empty Relation-like ( the of CPNT1,(*' {TTS12})) -defined ( the of CPNT1,(Im (q21B,TTS12))) -valued Function-like total quasi_total Element of bool [:( the of CPNT1,(*' {TTS12})),( the of CPNT1,(Im (q21B,TTS12))):]

Funcs (( the of CPNT1,(*' {TTS12})),( the of CPNT1,(Im (q21B,TTS12)))) is non empty functional FUNCTION_DOMAIN of ( the of CPNT1,(*' {TTS12})),( the of CPNT1,(Im (q21B,TTS12)))

PFuncs (( the of CPNT1,(*' {TTS12})),( the of CPNT1,(Im (q21B,TTS12)))) is non empty functional set

[:(CPNT1),(PFuncs ((bool (PFuncs ( the carrier of CPNT1, the of CPNT1))),(bool (PFuncs ( the carrier of CPNT2, the of CPNT1))))):] is Relation-like set

bool [:(CPNT1),(PFuncs ((bool (PFuncs ( the carrier of CPNT1, the of CPNT1))),(bool (PFuncs ( the carrier of CPNT2, the of CPNT1))))):] is non empty set

O21B is Relation-like (CPNT1) -defined PFuncs ((bool (PFuncs ( the carrier of CPNT1, the of CPNT1))),(bool (PFuncs ( the carrier of CPNT2, the of CPNT1)))) -valued Function-like total quasi_total Element of bool [:(CPNT1),(PFuncs ((bool (PFuncs ( the carrier of CPNT1, the of CPNT1))),(bool (PFuncs ( the carrier of CPNT2, the of CPNT1))))):]

TTS12 is Element of the carrier' of CPNT1

O21B . TTS12 is Relation-like Function-like set

{TTS12} is non empty trivial finite Element of bool the carrier' of CPNT1

*' {TTS12} is Element of bool the carrier of CPNT1

bool the carrier of CPNT1 is non empty set

the S-T_Arcs of CPNT1 is non empty Relation-like the carrier of CPNT1 -defined the carrier' of CPNT1 -valued Element of bool [: the carrier of CPNT1, the carrier' of CPNT1:]

[: the carrier of CPNT1, the carrier' of CPNT1:] is non empty Relation-like set

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

{ b

( b

( the of CPNT1,(*' {TTS12})) is non empty Element of bool (bool (Funcs ((*' {TTS12}), the of CPNT1)))

Funcs ((*' {TTS12}), the of CPNT1) is non empty functional FUNCTION_DOMAIN of *' {TTS12}, the of CPNT1

bool (Funcs ((*' {TTS12}), the of CPNT1)) is non empty set

bool (bool (Funcs ((*' {TTS12}), the of CPNT1))) is non empty set

{ b

Im (q21B,TTS12) is Element of bool the carrier of CPNT2

bool the carrier of CPNT2 is non empty set

( the of CPNT1,(Im (q21B,TTS12))) is non empty Element of bool (bool (Funcs ((Im (q21B,TTS12)), the of CPNT1)))

Funcs ((Im (q21B,TTS12)), the of CPNT1) is non empty functional FUNCTION_DOMAIN of Im (q21B,TTS12), the of CPNT1

bool (Funcs ((Im (q21B,TTS12)), the of CPNT1)) is non empty set

bool (bool (Funcs ((Im (q21B,TTS12)), the of CPNT1))) is non empty set

{ b

[:( the of CPNT1,(*' {TTS12})),( the of CPNT1,(Im (q21B,TTS12))):] is non empty Relation-like set

bool [:( the of CPNT1,(*' {TTS12})),( the of CPNT1,(Im (q21B,TTS12))):] is non empty set

q12 is Element of the carrier' of CPNT1

{q12} is non empty trivial finite Element of bool the carrier' of CPNT1

*' {q12} is Element of bool the carrier of CPNT1

{ b

( b

( the of CPNT1,(*' {q12})) is non empty Element of bool (bool (Funcs ((*' {q12}), the of CPNT1)))

Funcs ((*' {q12}), the of CPNT1) is non empty functional FUNCTION_DOMAIN of *' {q12}, the of CPNT1

bool (Funcs ((*' {q12}), the of CPNT1)) is non empty set

bool (bool (Funcs ((*' {q12}), the of CPNT1))) is non empty set

{ b

Im (q21B,q12) is Element of bool the carrier of CPNT2

( the of CPNT1,(Im (q21B,q12))) is non empty Element of bool (bool (Funcs ((Im (q21B,q12)), the of CPNT1)))

Funcs ((Im (q21B,q12)), the of CPNT1) is non empty functional FUNCTION_DOMAIN of Im (q21B,q12), the of CPNT1

bool (Funcs ((Im (q21B,q12)), the of CPNT1)) is non empty set

bool (bool (Funcs ((Im (q21B,q12)), the of CPNT1))) is non empty set

{ b

[:( the of CPNT1,(*' {q12})),( the of CPNT1,(Im (q21B,q12))):] is non empty Relation-like set

bool [:( the of CPNT1,(*' {q12})),( the of CPNT1,(Im (q21B,q12))):] is non empty set

TTS12 is set

q12 is Element of the carrier' of CPNT2

Im (O12B,q12) is Element of bool the carrier of CPNT1

{q12} is non empty trivial finite Element of bool the carrier' of CPNT2

*' {q12} is Element of bool the carrier of CPNT2

the S-T_Arcs of CPNT2 is non empty Relation-like the carrier of CPNT2 -defined the carrier' of CPNT2 -valued Element of bool [: the carrier of CPNT2, the carrier' of CPNT2:]

[: the carrier of CPNT2, the carrier' of CPNT2:] is non empty Relation-like set

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

{ b

( b

( the of CPNT2,(*' {q12})) is non empty Element of bool (bool (Funcs ((*' {q12}), the of CPNT2)))

Funcs ((*' {q12}), the of CPNT2) is non empty functional FUNCTION_DOMAIN of *' {q12}, the of CPNT2

bool (Funcs ((*' {q12}), the of CPNT2)) is non empty set

bool (bool (Funcs ((*' {q12}), the of CPNT2))) is non empty set

{ b

( the of CPNT2,(Im (O12B,q12))) is non empty Element of bool (bool (Funcs ((Im (O12B,q12)), the of CPNT2)))

Funcs ((Im (O12B,q12)), the of CPNT2) is non empty functional FUNCTION_DOMAIN of Im (O12B,q12), the of CPNT2

bool (Funcs ((Im (O12B,q12)), the of CPNT2)) is non empty set

bool (bool (Funcs ((Im (O12B,q12)), the of CPNT2))) is non empty set

{ b

[:( the of CPNT2,(*' {q12})),( the of CPNT2,(Im (O12B,q12))):] is non empty Relation-like set

bool [:( the of CPNT2,(*' {q12})),( the of CPNT2,(Im (O12B,q12))):] is non empty set

the non empty Relation-like ( the of CPNT2,(*' {q12})) -defined ( the of CPNT2,(Im (O12B,q12))) -valued Function-like total quasi_total Element of bool [:( the of CPNT2,(*' {q12})),( the of CPNT2,(Im (O12B,q12))):] is non empty Relation-like ( the of CPNT2,(*' {q12})) -defined ( the of CPNT2,(Im (O12B,q12))) -valued Function-like total quasi_total Element of bool [:( the of CPNT2,(*' {q12})),( the of CPNT2,(Im (O12B,q12))):]

Funcs (( the of CPNT2,(*' {q12})),( the of CPNT2,(Im (O12B,q12)))) is non empty functional FUNCTION_DOMAIN of ( the of CPNT2,(*' {q12})),( the of CPNT2,(Im (O12B,q12)))

PFuncs (( the of CPNT2,(*' {q12})),( the of CPNT2,(Im (O12B,q12)))) is non empty functional set

[:(CPNT2),(PFuncs ((bool (PFuncs ( the carrier of CPNT2, the of CPNT2))),(bool (PFuncs ( the carrier of CPNT1, the of CPNT2))))):] is Relation-like set

bool [:(CPNT2),(PFuncs ((bool (PFuncs ( the carrier of CPNT2, the of CPNT2))),(bool (PFuncs ( the carrier of CPNT1, the of CPNT2))))):] is non empty set

TTS12 is Relation-like (CPNT2) -defined PFuncs ((bool (PFuncs ( the carrier of CPNT2, the of CPNT2))),(bool (PFuncs ( the carrier of CPNT1, the of CPNT2)))) -valued Function-like total quasi_total Element of bool [:(CPNT2),(PFuncs ((bool (PFuncs ( the carrier of CPNT2, the of CPNT2))),(bool (PFuncs ( the carrier of CPNT1, the of CPNT2))))):]

q12 is Element of the carrier' of CPNT2

TTS12 . q12 is Relation-like Function-like set

{q12} is non empty trivial finite Element of bool the carrier' of CPNT2

*' {q12} is Element of bool the carrier of CPNT2

the S-T_Arcs of CPNT2 is non empty Relation-like the carrier of CPNT2 -defined the carrier' of CPNT2 -valued Element of bool [: the carrier of CPNT2, the carrier' of CPNT2:]

[: the carrier of CPNT2, the carrier' of CPNT2:] is non empty Relation-like set

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

{ b

( b

( the of CPNT2,(*' {q12})) is non empty Element of bool (bool (Funcs ((*' {q12}), the of CPNT2)))

Funcs ((*' {q12}), the of CPNT2) is non empty functional FUNCTION_DOMAIN of *' {q12}, the of CPNT2

bool (Funcs ((*' {q12}), the of CPNT2)) is non empty set

bool (bool (Funcs ((*' {q12}), the of CPNT2))) is non empty set

{ b

Im (O12B,q12) is Element of bool the carrier of CPNT1

( the of CPNT2,(Im (O12B,q12))) is non empty Element of bool (bool (Funcs ((Im (O12B,q12)), the of CPNT2)))

Funcs ((Im (O12B,q12)), the of CPNT2) is non empty functional FUNCTION_DOMAIN of Im (O12B,q12), the of CPNT2

bool (Funcs ((Im (O12B,q12)), the of CPNT2)) is non empty set

bool (bool (Funcs ((Im (O12B,q12)), the of CPNT2))) is non empty set

{ b

[:( the of CPNT2,(*' {q12})),( the of CPNT2,(Im (O12B,q12))):] is non empty Relation-like set

bool [:( the of CPNT2,(*' {q12})),( the of CPNT2,(Im (O12B,q12))):] is non empty set

q21 is Element of the carrier' of CPNT2

{q21} is non empty trivial finite Element of bool the carrier' of CPNT2

*' {q21} is Element of bool the carrier of CPNT2

{ b

( b

( the of CPNT2,(*' {q21})) is non empty Element of bool (bool (Funcs ((*' {q21}), the of CPNT2)))

Funcs ((*' {q21}), the of CPNT2) is non empty functional FUNCTION_DOMAIN of *' {q21}, the of CPNT2

bool (Funcs ((*' {q21}), the of CPNT2)) is non empty set

bool (bool (Funcs ((*' {q21}), the of CPNT2))) is non empty set

{ b

Im (O12B,q21) is Element of bool the carrier of CPNT1

( the of CPNT2,(Im (O12B,q21))) is non empty Element of bool (bool (Funcs ((Im (O12B,q21)), the of CPNT2)))

Funcs ((Im (O12B,q21)), the of CPNT2) is non empty functional FUNCTION_DOMAIN of Im (O12B,q21), the of CPNT2

bool (Funcs ((Im (O12B,q21)), the of CPNT2)) is non empty set

bool (bool (Funcs ((Im (O12B,q21)), the of CPNT2))) is non empty set

{ b

[:( the of CPNT2,(*' {q21})),( the of CPNT2,(Im (O12B,q21))):] is non empty Relation-like set

bool [:( the of CPNT2,(*' {q21})),( the of CPNT2,(Im (O12B,q21))):] is non empty set

[O21B,TTS12] is non empty Element of [:(bool [:(CPNT1),(PFuncs ((bool (PFuncs ( the carrier of CPNT1, the of CPNT1))),(bool (PFuncs ( the carrier of CPNT2, the of CPNT1))))):]),(bool [:(CPNT2),(PFuncs ((bool (PFuncs ( the carrier of CPNT2, the of CPNT2))),(bool (PFuncs ( the carrier of CPNT1, the of CPNT2))))):]):]

[:(bool [:(CPNT1),(PFuncs ((bool (PFuncs ( the carrier of CPNT1, the of CPNT1))),(bool (PFuncs ( the carrier of CPNT2, the of CPNT1))))):]),(bool [:(CPNT2),(PFuncs ((bool (PFuncs ( the carrier of CPNT2, the of CPNT2))),(bool (PFuncs ( the carrier of CPNT1, the of CPNT2))))):]):] is non empty Relation-like set

{O21B,TTS12} is non empty functional finite set

{O21B} is non empty trivial functional finite set

{{O21B,TTS12},{O21B}} is non empty finite V32() set

dom TTS12 is Element of bool (CPNT2)

bool (CPNT2) is non empty set

dom O21B is Element of bool (CPNT1)

bool (CPNT1) is non empty set

CPNT1 is non empty non void V49() with_S-T_arc with_T-S_arc () ()

CPNT2 is non empty non void V49() with_S-T_arc with_T-S_arc () ()

O is (CPNT1,CPNT2)

(CPNT1) is Element of bool the carrier' of CPNT1

the carrier' of CPNT1 is non empty set

bool the carrier' of CPNT1 is non empty set

{ b

the carrier of CPNT2 is non empty set

[:(CPNT1), the carrier of CPNT2:] is Relation-like set

bool [:(CPNT1), the carrier of CPNT2:] is non empty set

(CPNT2) is Element of bool the carrier' of CPNT2

the carrier' of CPNT2 is non empty set

bool the carrier' of CPNT2 is non empty set

{ b

the carrier of CPNT1 is non empty set

[:(CPNT2), the carrier of CPNT1:] is Relation-like set

bool [:(CPNT2), the carrier of CPNT1:] is non empty set

the of CPNT1 is non empty finite set

the of CPNT2 is non empty finite set

q is (CPNT1,CPNT2,O)

the carrier of CPNT1 \/ the carrier of CPNT2 is non empty set

the carrier' of CPNT1 \/ the carrier' of CPNT2 is non empty set

the S-T_Arcs of CPNT1 is non empty Relation-like the carrier of CPNT1 -defined the carrier' of CPNT1 -valued Element of bool [: the carrier of CPNT1, the carrier' of CPNT1:]

[: the carrier of CPNT1, the carrier' of CPNT1:] is non empty Relation-like set

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

the S-T_Arcs of CPNT2 is non empty Relation-like the carrier of CPNT2 -defined the carrier' of CPNT2 -valued Element of bool [: the carrier of CPNT2, the carrier' of CPNT2:]

[: the carrier of CPNT2, the carrier' of CPNT2:] is non empty Relation-like set

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

the S-T_Arcs of CPNT1 \/ the S-T_Arcs of CPNT2 is non empty Relation-like set

the T-S_Arcs of CPNT1 is non empty Relation-like the carrier' of CPNT1 -defined the carrier of CPNT1 -valued Element of bool [: the carrier' of CPNT1, the carrier of CPNT1:]

[: the carrier' of CPNT1, the carrier of CPNT1:] is non empty Relation-like set

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

the T-S_Arcs of CPNT2 is non empty Relation-like the carrier' of CPNT2 -defined the carrier of CPNT2 -valued Element of bool [: the carrier' of CPNT2, the carrier of CPNT2:]

[: the carrier' of CPNT2, the carrier of CPNT2:] is non empty Relation-like set

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

the T-S_Arcs of CPNT1 \/ the T-S_Arcs of CPNT2 is non empty Relation-like set

the of CPNT1 \/ the of CPNT2 is non empty finite set

the of CPNT1 is Relation-like Function-like set

the of CPNT2 is Relation-like Function-like set

the of CPNT1 +* the of CPNT2 is Relation-like Function-like set

CB is non empty set

q12A is non empty set

[:q12A,CB:] is non empty Relation-like set

bool [:q12A,CB:] is non empty set

[:CB,q12A:] is non empty Relation-like set

bool [:CB,q12A:] is non empty set

q21A is Relation-like q12A -defined CB -valued Element of bool [:q12A,CB:]

q12B is Relation-like q12A -defined CB -valued Element of bool [:q12A,CB:]

q21A \/ q12B is Relation-like q12A -defined CB -valued Element of bool [:q12A,CB:]

O12B is Relation-like CB -defined q12A -valued Element of bool [:CB,q12A:]

O12A is Relation-like CB -defined q12A -valued Element of bool [:CB,q12A:]

O12B \/ O12A is Relation-like CB -defined q12A -valued Element of bool [:CB,q12A:]

O12 is Relation-like (CPNT1) -defined the carrier of CPNT2 -valued Function-like total quasi_total Element of bool [:(CPNT1), the carrier of CPNT2:]

O21 is Relation-like (CPNT2) -defined the carrier of CPNT1 -valued Function-like total quasi_total Element of bool [:(CPNT2), the carrier of CPNT1:]

[O12,O21] is non empty Element of [:(bool [:(CPNT1), the carrier of CPNT2:]),(bool [:(CPNT2), the carrier of CPNT1:]):]

[:(bool [:(CPNT1), the carrier of CPNT2:]),(bool [:(CPNT2), the carrier of CPNT1:]):] is non empty Relation-like set

{O12,O21} is non empty functional finite set

{O12} is non empty trivial functional finite set

{{O12,O21},{O12}} is non empty finite V32() set

q12 is Relation-like Function-like set