:: 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₁ where b₁ is Relation-like CPNT2 -defined CPNT1 -valued Function-like total quasi_total Element of bool [:CPNT2,CPNT1:] : b₁ | O = q } is set
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₁ where b₁ is Relation-like CPNT2 -defined CPNT1 -valued Function-like total quasi_total Element of bool [:CPNT2,CPNT1:] : b₁ | q = CA } is set
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₁ where b₁ is Relation-like O -defined CPNT1 -valued Function-like total quasi_total Element of bool [:O,CPNT1:] : b₁ | CA = CB } is set
[: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₁ where b₁ is Relation-like O -defined CPNT2 -valued Function-like total quasi_total Element of bool [:O,CPNT2:] : b₁ | CA = q12A } is set
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₁ where b₁ is functional Element of bool (Funcs (CPNT2,CPNT1)) : b₁ is non empty functional (CPNT1,CPNT2) } is set
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₁ where b₁ is functional Element of bool (Funcs (CPNT2,CPNT1)) : b₁ is non empty functional (CPNT1,CPNT2) } is set
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₁ where b₁ is Relation-like CPNT2 -defined CPNT1 -valued Function-like total quasi_total Element of bool [:CPNT2,CPNT1:] : b₁ | O = CA } is set
CB is Relation-like q -defined CPNT1 -valued Function-like total quasi_total Element of bool [:q,CPNT1:]
{ b₁ where b₁ is Relation-like CPNT2 -defined CPNT1 -valued Function-like total quasi_total Element of bool [:CPNT2,CPNT1:] : b₁ | q = 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 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₁ where b₁ is Relation-like CPNT2 -defined CPNT1 -valued Function-like total quasi_total Element of bool [:CPNT2,CPNT1:] : b₁ | O = q } is set
q12A is set
{ b₁ where b₁ is Relation-like CPNT2 -defined CPNT1 -valued Function-like total quasi_total Element of bool [:CPNT2,CPNT1:] : b₁ | CA = CB } is set
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₁ where b₁ is functional Element of bool (Funcs (O,CPNT1)) : b₁ is non empty functional (CPNT1,O) } 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₁ where b₁ is functional Element of bool (Funcs (q,CPNT2)) : b₁ is non empty functional (CPNT2,q) } is set
[:(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₁ where b₁ is functional Element of bool (Funcs (q,CPNT2)) : b₁ is non empty functional (CPNT2,q) } is 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₁ where b₁ is functional Element of bool (Funcs (O,CPNT1)) : b₁ is non empty functional (CPNT1,O) } is set
[:(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₁ where b₁ is functional Element of bool (Funcs (O,CPNT1)) : b₁ is non empty functional (CPNT1,O) } 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₁ where b₁ is functional Element of bool (Funcs (q,CPNT2)) : b₁ is non empty functional (CPNT2,q) } is set
[:(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₁ where b₁ is functional Element of bool (Funcs (q,CPNT2)) : b₁ is non empty functional (CPNT2,q) } is set
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₁ where b₁ is functional Element of bool (Funcs (O,CPNT1)) : b₁ is non empty functional (CPNT1,O) } is set
[:(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₁ where b₁ is Relation-like CPNT2 -defined CPNT1 -valued Function-like total quasi_total Element of bool [:CPNT2,CPNT1:] : b₁ | q = CA } is set
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₁ where b₁ is Relation-like CPNT2 -defined CPNT1 -valued Function-like total quasi_total Element of bool [:CPNT2,CPNT1:] : b₁ | CB = q12A } is set
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₁ where b₁ is Relation-like CPNT2 -defined CPNT1 -valued Function-like total quasi_total Element of bool [:CPNT2,CPNT1:] : b₁ | q21A = O12A } is set
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₁ where b₁ is functional Element of bool (Funcs (O,CPNT1)) : b₁ is non empty functional (CPNT1,O) } is set
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₁ where b₁ is functional Element of bool (Funcs (q12A,CA)) : b₁ is non empty functional (CA,q12A) } is set
[:(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₁ where b₁ is functional Element of bool (Funcs (q,CPNT2)) : b₁ is non empty functional (CPNT2,q) } is set
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₁ where b₁ is functional Element of bool (Funcs (q21A,CB)) : b₁ is non empty functional (CB,q21A) } is set
(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₁ where b₁ is Element of the carrier' of CPNT1 : b₁ is (CPNT1) } is set
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₁ where b₁ is Element of the carrier of CPNT1 : ex b₂ being Element of the S-T_Arcs of CPNT1 ex b₃ being Element of the carrier' of CPNT1 st
( b₃ in {CPNT2} & b₂ = [b₁,b₃] ) } is set
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₁ where b₁ is Element of the carrier of CPNT1 : ex b₂ being Element of the T-S_Arcs of CPNT1 ex b₃ being Element of the carrier' of CPNT1 st
( b₃ in {CPNT2} & b₂ = [b₃,b₁] ) } is set
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₁ where b₁ is Element of the carrier of CPNT1 : ex b₂ being Element of the S-T_Arcs of CPNT1 ex b₃ being Element of the carrier' of CPNT1 st
( b₃ in {O} & b₂ = [b₁,b₃] ) } is set
{O} *' is Element of bool the carrier of CPNT1
{ b₁ where b₁ is Element of the carrier of CPNT1 : ex b₂ being Element of the T-S_Arcs of CPNT1 ex b₃ being Element of the carrier' of CPNT1 st
( b₃ in {O} & b₂ = [b₃,b₁] ) } is set
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₁ where b₁ is Element of the carrier of CPNT2 : ex b₂ being Element of the S-T_Arcs of CPNT2 ex b₃ being Element of the carrier' of CPNT2 st
( b₃ in {q} & b₂ = [b₁,b₃] ) } is set
{q} *' is Element of bool the carrier of CPNT2
{ b₁ where b₁ is Element of the carrier of CPNT2 : ex b₂ being Element of the T-S_Arcs of CPNT2 ex b₃ being Element of the carrier' of CPNT2 st
( b₃ in {q} & b₂ = [b₃,b₁] ) } is 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 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₁ where b₁ is functional Element of bool (Funcs ({{}},{ the set , the set , the set })) : b₁ is non empty functional ({ the set , the set , the set },{{}}) } is set
[:({ 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₁ where b₁ is Element of the carrier of q21B : ex b₂ being Element of the T-S_Arcs of q21B ex b₃ being Element of the carrier' of q21B st
( b₃ in {O21B} & b₂ = [b₃,b₁] ) } is set
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₁ where b₁ is Element of the carrier of q21B : ex b₂ being Element of the S-T_Arcs of q21B ex b₃ being Element of the carrier' of q21B st
( b₃ in {O21B} & b₂ = [b₁,b₃] ) } is set
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₁ where b₁ is functional Element of bool (Funcs (q12,O12B)) : b₁ is non empty functional (O12B,q12) } is set
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₁ where b₁ is functional Element of bool (Funcs (TTS12,O12B)) : b₁ is non empty functional (O12B,TTS12) } is set
[:(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₁ where b₁ is Element of the carrier of q21B : ex b₂ being Element of the T-S_Arcs of q21B ex b₃ being Element of the carrier' of q21B st
( b₃ in {O12B} & b₂ = [b₃,b₁] ) } is set
(q21B) is Element of bool the carrier' of q21B
{ b₁ where b₁ is Element of the carrier' of q21B : b₁ is (q21B) } is set
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₁ where b₁ is Element of the carrier' of CPNT1 : b₁ is (CPNT1) } is set
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₁ where b₁ is Element of the carrier' of CPNT2 : b₁ is (CPNT2) } is set
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₁ where b₁ is Element of the carrier' of CPNT1 : b₁ is (CPNT1) } is set
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₁ where b₁ is Element of the carrier' of CPNT2 : b₁ is (CPNT2) } is set
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₁ where b₁ is Element of the carrier of CPNT1 : ex b₂ being Element of the S-T_Arcs of CPNT1 ex b₃ being Element of the carrier' of CPNT1 st
( b₃ in {TTS12} & b₂ = [b₁,b₃] ) } is set
( 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₁ where b₁ is functional Element of bool (Funcs ((*' {TTS12}), the of CPNT1)) : b₁ is non empty functional ( the of CPNT1, *' {TTS12}) } is 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₁ where b₁ is functional Element of bool (Funcs ((Im (q21B,TTS12)), the of CPNT1)) : b₁ is non empty functional ( the of CPNT1, Im (q21B,TTS12)) } is set
[:( 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₁ where b₁ is Element of the carrier of CPNT1 : ex b₂ being Element of the S-T_Arcs of CPNT1 ex b₃ being Element of the carrier' of CPNT1 st
( b₃ in {TTS12} & b₂ = [b₁,b₃] ) } is set
( 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₁ where b₁ is functional Element of bool (Funcs ((*' {TTS12}), the of CPNT1)) : b₁ is non empty functional ( the of CPNT1, *' {TTS12}) } is set
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₁ where b₁ is functional Element of bool (Funcs ((Im (q21B,TTS12)), the of CPNT1)) : b₁ is non empty functional ( the of CPNT1, Im (q21B,TTS12)) } is set
[:( 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₁ where b₁ is Element of the carrier of CPNT1 : ex b₂ being Element of the S-T_Arcs of CPNT1 ex b₃ being Element of the carrier' of CPNT1 st
( b₃ in {q12} & b₂ = [b₁,b₃] ) } is set
( 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₁ where b₁ is functional Element of bool (Funcs ((*' {q12}), the of CPNT1)) : b₁ is non empty functional ( the of CPNT1, *' {q12}) } is set
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₁ where b₁ is functional Element of bool (Funcs ((Im (q21B,q12)), the of CPNT1)) : b₁ is non empty functional ( the of CPNT1, Im (q21B,q12)) } is set
[:( 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₁ where b₁ is Element of the carrier of CPNT2 : ex b₂ being Element of the S-T_Arcs of CPNT2 ex b₃ being Element of the carrier' of CPNT2 st
( b₃ in {q12} & b₂ = [b₁,b₃] ) } is set
( 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₁ where b₁ is functional Element of bool (Funcs ((*' {q12}), the of CPNT2)) : b₁ is non empty functional ( the of CPNT2, *' {q12}) } is set
( 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₁ where b₁ is functional Element of bool (Funcs ((Im (O12B,q12)), the of CPNT2)) : b₁ is non empty functional ( the of CPNT2, Im (O12B,q12)) } is set
[:( 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₁ where b₁ is Element of the carrier of CPNT2 : ex b₂ being Element of the S-T_Arcs of CPNT2 ex b₃ being Element of the carrier' of CPNT2 st
( b₃ in {q12} & b₂ = [b₁,b₃] ) } is set
( 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₁ where b₁ is functional Element of bool (Funcs ((*' {q12}), the of CPNT2)) : b₁ is non empty functional ( the of CPNT2, *' {q12}) } is set
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₁ where b₁ is functional Element of bool (Funcs ((Im (O12B,q12)), the of CPNT2)) : b₁ is non empty functional ( the of CPNT2, Im (O12B,q12)) } is set
[:( 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₁ where b₁ is Element of the carrier of CPNT2 : ex b₂ being Element of the S-T_Arcs of CPNT2 ex b₃ being Element of the carrier' of CPNT2 st
( b₃ in {q21} & b₂ = [b₁,b₃] ) } is set
( 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₁ where b₁ is functional Element of bool (Funcs ((*' {q21}), the of CPNT2)) : b₁ is non empty functional ( the of CPNT2, *' {q21}) } is set
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₁ where b₁ is functional Element of bool (Funcs ((Im (O12B,q21)), the of CPNT2)) : b₁ is non empty functional ( the of CPNT2, Im (O12B,q21)) } is set
[:( 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₁ where b₁ is Element of the carrier' of CPNT1 : b₁ is (CPNT1) } is set
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₁ where b₁ is Element of the carrier' of CPNT2 : b₁ is (CPNT2) } is set
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
dom q12 is set
q21 is Relation-like Function-like set
dom q21 is set
[q12,q21] is non empty set
{q12,q21} is non empty functional finite set
{q12} is non empty trivial functional finite set
{{q12,q21},{q12}} is non empty finite V32() set
dom the of CPNT2 is set
the carrier' of CPNT2 \ (dom q21) is Element of bool the carrier' of CPNT2
the carrier' of CPNT1 /\ the carrier' of CPNT2 is set
dom the of CPNT1 is set
the carrier' of CPNT1 \ (dom q12) is Element of bool the carrier' of CPNT1
(dom the of CPNT1) /\ (dom the of CPNT2) is set
(dom the of CPNT2) /\ (dom q21) is set
(dom the of CPNT2) /\ (dom q12) is set
(dom q12) /\ (dom q21) is set
(dom the of CPNT1) /\ (dom q21) is set
(dom the of CPNT1) /\ (dom q12) is set
( the of CPNT1 +* the of CPNT2) +* q12 is Relation-like Function-like set
(( the of CPNT1 +* the of CPNT2) +* q12) +* q21 is Relation-like Function-like set
TTS12 is non empty Relation-like CB -defined q12A -valued Element of bool [:CB,q12A:]
E31 is Relation-like CB -defined q12A -valued Element of bool [:CB,q12A:]
E32 is Relation-like CB -defined q12A -valued Element of bool [:CB,q12A:]
E31 \/ E32 is Relation-like CB -defined q12A -valued Element of bool [:CB,q12A:]
TTS12 \/ (E31 \/ E32) is non empty Relation-like CB -defined q12A -valued Element of bool [:CB,q12A:]
O21B is non empty Relation-like q12A -defined CB -valued Element of bool [:q12A,CB:]
TS12 is non empty Relation-like CB -defined q12A -valued Element of bool [:CB,q12A:]
CA is non empty finite set
(q12A,CB,O21B,TS12,CA,((( the of CPNT1 +* the of CPNT2) +* q12) +* q21)) is () ()
CPNT12 is non empty non void V49() with_S-T_arc with_T-S_arc ()
the carrier of CPNT12 is non empty set
the S-T_Arcs of CPNT12 is non empty Relation-like the carrier of CPNT12 -defined the carrier' of CPNT12 -valued Element of bool [: the carrier of CPNT12, the carrier' of CPNT12:]
the carrier' of CPNT12 is non empty set
[: the carrier of CPNT12, the carrier' of CPNT12:] is non empty Relation-like set
bool [: the carrier of CPNT12, the carrier' of CPNT12:] is non empty set
the T-S_Arcs of CPNT12 is non empty Relation-like the carrier' of CPNT12 -defined the carrier of CPNT12 -valued Element of bool [: the carrier' of CPNT12, the carrier of CPNT12:]
[: the carrier' of CPNT12, the carrier of CPNT12:] is non empty Relation-like set
bool [: the carrier' of CPNT12, the carrier of CPNT12:] is non empty set
RR4 is set
dom ((( the of CPNT1 +* the of CPNT2) +* q12) +* q21) is set
dom (( the of CPNT1 +* the of CPNT2) +* q12) is set
dom ( the of CPNT1 +* the of CPNT2) is set
the of CPNT12 is Relation-like Function-like set
dom the of CPNT12 is set
the of CPNT12 is non empty finite set
bool the of CPNT12 is non empty finite V32() set
RR4 is Element of the carrier' of CPNT12
{RR4} is non empty trivial finite Element of bool the carrier' of CPNT12
bool the carrier' of CPNT12 is non empty set
*' {RR4} is Element of bool the carrier of CPNT12
bool the carrier of CPNT12 is non empty set
{ b₁ where b₁ is Element of the carrier of CPNT12 : ex b₂ being Element of the S-T_Arcs of CPNT12 ex b₃ being Element of the carrier' of CPNT12 st
( b₃ in {RR4} & b₂ = [b₁,b₃] ) } is set
bool (*' {RR4}) is non empty set
{RR4} *' is Element of bool the carrier of CPNT12
{ b₁ where b₁ is Element of the carrier of CPNT12 : ex b₂ being Element of the T-S_Arcs of CPNT12 ex b₃ being Element of the carrier' of CPNT12 st
( b₃ in {RR4} & b₂ = [b₃,b₁] ) } is set
bool ({RR4} *') is non empty set
the of CPNT12 . RR4 is set
the carrier' of CPNT1 \ (CPNT1) is Element of bool the carrier' of CPNT1
bool the of CPNT1 is non empty finite V32() set
RR3 is Element of the carrier' of CPNT1
{RR3} is non empty trivial finite Element of bool the carrier' of CPNT1
*' {RR3} is Element of bool the carrier of CPNT1
bool the carrier of CPNT1 is non empty set
{ b₁ where b₁ is Element of the carrier of CPNT1 : ex b₂ being Element of the S-T_Arcs of CPNT1 ex b₃ being Element of the carrier' of CPNT1 st
( b₃ in {RR3} & b₂ = [b₁,b₃] ) } is set
bool (*' {RR3}) is non empty set
{RR3} *' is Element of bool the carrier of CPNT1
{ b₁ where b₁ is Element of the carrier of CPNT1 : ex b₂ being Element of the T-S_Arcs of CPNT1 ex b₃ being Element of the carrier' of CPNT1 st
( b₃ in {RR3} & b₂ = [b₃,b₁] ) } is set
bool ({RR3} *') is non empty set
the of CPNT1 . RR3 is set
RR2 is non empty finite Element of bool the of CPNT1
RR1 is Element of bool (*' {RR3})
(RR2,RR1) is non empty Element of bool (bool (Funcs (RR1,RR2)))
Funcs (RR1,RR2) is non empty functional FUNCTION_DOMAIN of RR1,RR2
bool (Funcs (RR1,RR2)) is non empty set
bool (bool (Funcs (RR1,RR2))) is non empty set
{ b₁ where b₁ is functional Element of bool (Funcs (RR1,RR2)) : b₁ is non empty functional (RR2,RR1) } is set
x is Element of bool ({RR3} *')
(RR2,x) is non empty Element of bool (bool (Funcs (x,RR2)))
Funcs (x,RR2) is non empty functional FUNCTION_DOMAIN of x,RR2
bool (Funcs (x,RR2)) is non empty set
bool (bool (Funcs (x,RR2))) is non empty set
{ b₁ where b₁ is functional Element of bool (Funcs (x,RR2)) : b₁ is non empty functional (RR2,x) } is set
[:(RR2,RR1),(RR2,x):] is non empty Relation-like set
bool [:(RR2,RR1),(RR2,x):] is non empty set
s is non empty finite Element of bool the of CPNT12
t is Element of bool (*' {RR4})
(s,t) is non empty Element of bool (bool (Funcs (t,s)))
Funcs (t,s) is non empty functional FUNCTION_DOMAIN of t,s
bool (Funcs (t,s)) is non empty set
bool (bool (Funcs (t,s))) is non empty set
{ b₁ where b₁ is functional Element of bool (Funcs (t,s)) : b₁ is non empty functional (s,t) } is set
s is Element of bool ({RR4} *')
(s,s) is non empty Element of bool (bool (Funcs (s,s)))
Funcs (s,s) is non empty functional FUNCTION_DOMAIN of s,s
bool (Funcs (s,s)) is non empty set
bool (bool (Funcs (s,s))) is non empty set
{ b₁ where b₁ is functional Element of bool (Funcs (s,s)) : b₁ is non empty functional (s,s) } is set
[:(s,t),(s,s):] is non empty Relation-like set
bool [:(s,t),(s,s):] is non empty set
the carrier' of CPNT2 \ (CPNT2) is Element of bool the carrier' of CPNT2
bool the of CPNT2 is non empty finite V32() set
RR3 is Element of the carrier' of CPNT2
{RR3} is non empty trivial finite Element of bool the carrier' of CPNT2
*' {RR3} is Element of bool the carrier of CPNT2
bool the carrier of CPNT2 is non empty set
{ b₁ where b₁ is Element of the carrier of CPNT2 : ex b₂ being Element of the S-T_Arcs of CPNT2 ex b₃ being Element of the carrier' of CPNT2 st
( b₃ in {RR3} & b₂ = [b₁,b₃] ) } is set
bool (*' {RR3}) is non empty set
{RR3} *' is Element of bool the carrier of CPNT2
{ b₁ where b₁ is Element of the carrier of CPNT2 : ex b₂ being Element of the T-S_Arcs of CPNT2 ex b₃ being Element of the carrier' of CPNT2 st
( b₃ in {RR3} & b₂ = [b₃,b₁] ) } is set
bool ({RR3} *') is non empty set
the of CPNT2 . RR3 is set
RR2 is non empty finite Element of bool the of CPNT2
RR1 is Element of bool (*' {RR3})
(RR2,RR1) is non empty Element of bool (bool (Funcs (RR1,RR2)))
Funcs (RR1,RR2) is non empty functional FUNCTION_DOMAIN of RR1,RR2
bool (Funcs (RR1,RR2)) is non empty set
bool (bool (Funcs (RR1,RR2))) is non empty set
{ b₁ where b₁ is functional Element of bool (Funcs (RR1,RR2)) : b₁ is non empty functional (RR2,RR1) } is set
x is Element of bool ({RR3} *')
(RR2,x) is non empty Element of bool (bool (Funcs (x,RR2)))
Funcs (x,RR2) is non empty functional FUNCTION_DOMAIN of x,RR2
bool (Funcs (x,RR2)) is non empty set
bool (bool (Funcs (x,RR2))) is non empty set
{ b₁ where b₁ is functional Element of bool (Funcs (x,RR2)) : b₁ is non empty functional (RR2,x) } is set
[:(RR2,RR1),(RR2,x):] is non empty Relation-like set
bool [:(RR2,RR1),(RR2,x):] is non empty set
s is non empty finite Element of bool the of CPNT12
t is Element of bool (*' {RR4})
(s,t) is non empty Element of bool (bool (Funcs (t,s)))
Funcs (t,s) is non empty functional FUNCTION_DOMAIN of t,s
bool (Funcs (t,s)) is non empty set
bool (bool (Funcs (t,s))) is non empty set
{ b₁ where b₁ is functional Element of bool (Funcs (t,s)) : b₁ is non empty functional (s,t) } is set
s is Element of bool ({RR4} *')
(s,s) is non empty Element of bool (bool (Funcs (s,s)))
Funcs (s,s) is non empty functional FUNCTION_DOMAIN of s,s
bool (Funcs (s,s)) is non empty set
bool (bool (Funcs (s,s))) is non empty set
{ b₁ where b₁ is functional Element of bool (Funcs (s,s)) : b₁ is non empty functional (s,s) } is set
[:(s,t),(s,s):] is non empty Relation-like set
bool [:(s,t),(s,s):] is non empty set
RR3 is Element of the carrier' of CPNT1
{RR3} is non empty trivial finite Element of bool the carrier' of CPNT1
*' {RR3} is Element of bool the carrier of CPNT1
bool the carrier of CPNT1 is non empty set
{ b₁ where b₁ is Element of the carrier of CPNT1 : ex b₂ being Element of the S-T_Arcs of CPNT1 ex b₃ being Element of the carrier' of CPNT1 st
( b₃ in {RR3} & b₂ = [b₁,b₃] ) } is set
Im (O12,RR3) is Element of bool the carrier of CPNT2
bool the carrier of CPNT2 is non empty set
x is set
t is Element of the carrier of CPNT2
[RR3,t] is non empty Element of [: the carrier' of CPNT1, the carrier of CPNT2:]
[: the carrier' of CPNT1, the carrier of CPNT2:] is non empty Relation-like set
{RR3,t} is non empty finite set
{RR3} is non empty trivial finite set
{{RR3,t},{RR3}} is non empty finite V32() set
[RR4,t] is non empty Element of [: the carrier' of CPNT12, the carrier of CPNT2:]
[: the carrier' of CPNT12, the carrier of CPNT2:] is non empty Relation-like set
{RR4,t} is non empty finite set
{RR4} is non empty trivial finite set
{{RR4,t},{RR4}} is non empty finite V32() set
s is Element of the T-S_Arcs of CPNT12
q12 . RR3 is set
( the of CPNT1,(*' {RR3})) is non empty Element of bool (bool (Funcs ((*' {RR3}), the of CPNT1)))
Funcs ((*' {RR3}), the of CPNT1) is non empty functional FUNCTION_DOMAIN of *' {RR3}, the of CPNT1
bool (Funcs ((*' {RR3}), the of CPNT1)) is non empty set
bool (bool (Funcs ((*' {RR3}), the of CPNT1))) is non empty set
{ b₁ where b₁ is functional Element of bool (Funcs ((*' {RR3}), the of CPNT1)) : b₁ is non empty functional ( the of CPNT1, *' {RR3}) } is set
( the of CPNT1,(Im (O12,RR3))) is non empty Element of bool (bool (Funcs ((Im (O12,RR3)), the of CPNT1)))
Funcs ((Im (O12,RR3)), the of CPNT1) is non empty functional FUNCTION_DOMAIN of Im (O12,RR3), the of CPNT1
bool (Funcs ((Im (O12,RR3)), the of CPNT1)) is non empty set
bool (bool (Funcs ((Im (O12,RR3)), the of CPNT1))) is non empty set
{ b₁ where b₁ is functional Element of bool (Funcs ((Im (O12,RR3)), the of CPNT1)) : b₁ is non empty functional ( the of CPNT1, Im (O12,RR3)) } is set
[:( the of CPNT1,(*' {RR3})),( the of CPNT1,(Im (O12,RR3))):] is non empty Relation-like set
bool [:( the of CPNT1,(*' {RR3})),( the of CPNT1,(Im (O12,RR3))):] is non empty set
t is Element of the carrier' of CPNT1
RR1 is non empty finite Element of bool the of CPNT12
RR2 is Element of bool (*' {RR4})
(RR1,RR2) is non empty Element of bool (bool (Funcs (RR2,RR1)))
Funcs (RR2,RR1) is non empty functional FUNCTION_DOMAIN of RR2,RR1
bool (Funcs (RR2,RR1)) is non empty set
bool (bool (Funcs (RR2,RR1))) is non empty set
{ b₁ where b₁ is functional Element of bool (Funcs (RR2,RR1)) : b₁ is non empty functional (RR1,RR2) } is set
x is Element of bool ({RR4} *')
(RR1,x) is non empty Element of bool (bool (Funcs (x,RR1)))
Funcs (x,RR1) is non empty functional FUNCTION_DOMAIN of x,RR1
bool (Funcs (x,RR1)) is non empty set
bool (bool (Funcs (x,RR1))) is non empty set
{ b₁ where b₁ is functional Element of bool (Funcs (x,RR1)) : b₁ is non empty functional (RR1,x) } is set
[:(RR1,RR2),(RR1,x):] is non empty Relation-like set
bool [:(RR1,RR2),(RR1,x):] is non empty set
RR3 is Element of the carrier' of CPNT2
{RR3} is non empty trivial finite Element of bool the carrier' of CPNT2
*' {RR3} is Element of bool the carrier of CPNT2
bool the carrier of CPNT2 is non empty set
{ b₁ where b₁ is Element of the carrier of CPNT2 : ex b₂ being Element of the S-T_Arcs of CPNT2 ex b₃ being Element of the carrier' of CPNT2 st
( b₃ in {RR3} & b₂ = [b₁,b₃] ) } is set
Im (O21,RR3) is Element of bool the carrier of CPNT1
bool the carrier of CPNT1 is non empty set
x is set
t is Element of the carrier of CPNT1
[RR3,t] is non empty Element of [: the carrier' of CPNT2, the carrier of CPNT1:]
[: the carrier' of CPNT2, the carrier of CPNT1:] is non empty Relation-like set
{RR3,t} is non empty finite set
{RR3} is non empty trivial finite set
{{RR3,t},{RR3}} is non empty finite V32() set
[RR4,t] is non empty Element of [: the carrier' of CPNT12, the carrier of CPNT1:]
[: the carrier' of CPNT12, the carrier of CPNT1:] is non empty Relation-like set
{RR4,t} is non empty finite set
{RR4} is non empty trivial finite set
{{RR4,t},{RR4}} is non empty finite V32() set
s is Element of the T-S_Arcs of CPNT12
q21 . RR3 is set
( the of CPNT2,(*' {RR3})) is non empty Element of bool (bool (Funcs ((*' {RR3}), the of CPNT2)))
Funcs ((*' {RR3}), the of CPNT2) is non empty functional FUNCTION_DOMAIN of *' {RR3}, the of CPNT2
bool (Funcs ((*' {RR3}), the of CPNT2)) is non empty set
bool (bool (Funcs ((*' {RR3}), the of CPNT2))) is non empty set
{ b₁ where b₁ is functional Element of bool (Funcs ((*' {RR3}), the of CPNT2)) : b₁ is non empty functional ( the of CPNT2, *' {RR3}) } is set
( the of CPNT2,(Im (O21,RR3))) is non empty Element of bool (bool (Funcs ((Im (O21,RR3)), the of CPNT2)))
Funcs ((Im (O21,RR3)), the of CPNT2) is non empty functional FUNCTION_DOMAIN of Im (O21,RR3), the of CPNT2
bool (Funcs ((Im (O21,RR3)), the of CPNT2)) is non empty set
bool (bool (Funcs ((Im (O21,RR3)), the of CPNT2))) is non empty set
{ b₁ where b₁ is functional Element of bool (Funcs ((Im (O21,RR3)), the of CPNT2)) : b₁ is non empty functional ( the of CPNT2, Im (O21,RR3)) } is set
[:( the of CPNT2,(*' {RR3})),( the of CPNT2,(Im (O21,RR3))):] is non empty Relation-like set
bool [:( the of CPNT2,(*' {RR3})),( the of CPNT2,(Im (O21,RR3))):] is non empty set
t is Element of the carrier' of CPNT2
RR1 is non empty finite Element of bool the of CPNT12
RR2 is Element of bool (*' {RR4})
(RR1,RR2) is non empty Element of bool (bool (Funcs (RR2,RR1)))
Funcs (RR2,RR1) is non empty functional FUNCTION_DOMAIN of RR2,RR1
bool (Funcs (RR2,RR1)) is non empty set
bool (bool (Funcs (RR2,RR1))) is non empty set
{ b₁ where b₁ is functional Element of bool (Funcs (RR2,RR1)) : b₁ is non empty functional (RR1,RR2) } is set
x is Element of bool ({RR4} *')
(RR1,x) is non empty Element of bool (bool (Funcs (x,RR1)))
Funcs (x,RR1) is non empty functional FUNCTION_DOMAIN of x,RR1
bool (Funcs (x,RR1)) is non empty set
bool (bool (Funcs (x,RR1))) is non empty set
{ b₁ where b₁ is functional Element of bool (Funcs (x,RR1)) : b₁ is non empty functional (RR1,x) } is set
[:(RR1,RR2),(RR1,x):] is non empty Relation-like set
bool [:(RR1,RR2),(RR1,x):] is non empty set
RR3 is non empty finite Element of bool the of CPNT12
RR2 is Element of bool (*' {RR4})
(RR3,RR2) is non empty Element of bool (bool (Funcs (RR2,RR3)))
Funcs (RR2,RR3) is non empty functional FUNCTION_DOMAIN of RR2,RR3
bool (Funcs (RR2,RR3)) is non empty set
bool (bool (Funcs (RR2,RR3))) is non empty set
{ b₁ where b₁ is functional Element of bool (Funcs (RR2,RR3)) : b₁ is non empty functional (RR3,RR2) } is set
RR1 is Element of bool ({RR4} *')
(RR3,RR1) is non empty Element of bool (bool (Funcs (RR1,RR3)))
Funcs (RR1,RR3) is non empty functional FUNCTION_DOMAIN of RR1,RR3
bool (Funcs (RR1,RR3)) is non empty set
bool (bool (Funcs (RR1,RR3))) is non empty set
{ b₁ where b₁ is functional Element of bool (Funcs (RR1,RR3)) : b₁ is non empty functional (RR3,RR1) } is set
[:(RR3,RR2),(RR3,RR1):] is non empty Relation-like set
bool [:(RR3,RR2),(RR3,RR1):] is non empty set
( the T-S_Arcs of CPNT1 \/ the T-S_Arcs of CPNT2) \/ O12 is non empty Relation-like set
(( the T-S_Arcs of CPNT1 \/ the T-S_Arcs of CPNT2) \/ O12) \/ O21 is non empty Relation-like set
the carrier' of CPNT1 \ (CPNT1) is Element of bool the carrier' of CPNT1
the carrier' of CPNT2 \ (CPNT2) is Element of bool the carrier' of CPNT2
RR4 is set
(CPNT12) is Element of bool the carrier' of CPNT12
bool the carrier' of CPNT12 is non empty set
{ b₁ where b₁ is Element of the carrier' of CPNT12 : b₁ is (CPNT12) } is set
the carrier' of CPNT12 \ (CPNT12) is Element of bool the carrier' of CPNT12
x is set
t is Element of the carrier' of CPNT12
s is Element of the carrier' of CPNT1
{s} is non empty trivial finite Element of bool the carrier' of CPNT1
{s} *' is Element of bool the carrier of CPNT1
bool the carrier of CPNT1 is non empty set
{ b₁ where b₁ is Element of the carrier of CPNT1 : ex b₂ being Element of the T-S_Arcs of CPNT1 ex b₃ being Element of the carrier' of CPNT1 st
( b₃ in {s} & b₂ = [b₃,b₁] ) } is set
{t} is non empty trivial finite Element of bool the carrier' of CPNT12
{t} *' is Element of bool the carrier of CPNT12
bool the carrier of CPNT12 is non empty set
{ b₁ where b₁ is Element of the carrier of CPNT12 : ex b₂ being Element of the T-S_Arcs of CPNT12 ex b₃ being Element of the carrier' of CPNT12 st
( b₃ in {t} & b₂ = [b₃,b₁] ) } is set
s is Element of the carrier' of CPNT12
f is set
t is Element of the carrier' of CPNT12
s is Element of the carrier' of CPNT2
{s} is non empty trivial finite Element of bool the carrier' of CPNT2
{s} *' is Element of bool the carrier of CPNT2
bool the carrier of CPNT2 is non empty set
{ b₁ where b₁ is Element of the carrier of CPNT2 : ex b₂ being Element of the T-S_Arcs of CPNT2 ex b₃ being Element of the carrier' of CPNT2 st
( b₃ in {s} & b₂ = [b₃,b₁] ) } is set
{t} is non empty trivial finite Element of bool the carrier' of CPNT12
{t} *' is Element of bool the carrier of CPNT12
bool the carrier of CPNT12 is non empty set
{ b₁ where b₁ is Element of the carrier of CPNT12 : ex b₂ being Element of the T-S_Arcs of CPNT12 ex b₃ being Element of the carrier' of CPNT12 st
( b₃ in {t} & b₂ = [b₃,b₁] ) } is set
s is Element of the carrier' of CPNT12
f is set
t is Element of the carrier' of CPNT12
dom O12 is Element of bool (CPNT1)
bool (CPNT1) is non empty set
s is set
[t,s] is non empty set
{t,s} is non empty finite set
{t} is non empty trivial finite set
{{t,s},{t}} is non empty finite V32() set
s is Element of the carrier of CPNT2
[t,s] is non empty Element of [: the carrier' of CPNT12, the carrier of CPNT2:]
[: the carrier' of CPNT12, the carrier of CPNT2:] is non empty Relation-like set
{t,s} is non empty finite set
{{t,s},{t}} is non empty finite V32() set
f is Element of the T-S_Arcs of CPNT12
{t} is non empty trivial finite Element of bool the carrier' of CPNT12
{t} *' is Element of bool the carrier of CPNT12
bool the carrier of CPNT12 is non empty set
{ b₁ where b₁ is Element of the carrier of CPNT12 : ex b₂ being Element of the T-S_Arcs of CPNT12 ex b₃ being Element of the carrier' of CPNT12 st
( b₃ in {t} & b₂ = [b₃,b₁] ) } is set
c₃₇ is Element of the carrier' of CPNT12
t is Element of the carrier' of CPNT12
dom O21 is Element of bool (CPNT2)
bool (CPNT2) is non empty set
s is set
[t,s] is non empty set
{t,s} is non empty finite set
{t} is non empty trivial finite set
{{t,s},{t}} is non empty finite V32() set
s is Element of the carrier of CPNT1
[t,s] is non empty Element of [: the carrier' of CPNT12, the carrier of CPNT1:]
[: the carrier' of CPNT12, the carrier of CPNT1:] is non empty Relation-like set
{t,s} is non empty finite set
{{t,s},{t}} is non empty finite V32() set
f is Element of the T-S_Arcs of CPNT12
{t} is non empty trivial finite Element of bool the carrier' of CPNT12
{t} *' is Element of bool the carrier of CPNT12
bool the carrier of CPNT12 is non empty set
{ b₁ where b₁ is Element of the carrier of CPNT12 : ex b₂ being Element of the T-S_Arcs of CPNT12 ex b₃ being Element of the carrier' of CPNT12 st
( b₃ in {t} & b₂ = [b₃,b₁] ) } is set
c₃₇ is Element of the carrier' of CPNT12
t is Element of the carrier' of CPNT12
CA is non empty non void V49() with_S-T_arc with_T-S_arc () () ()
the carrier of CA is non empty set
the carrier' of CA is non empty set
the S-T_Arcs of CA is non empty Relation-like the carrier of CA -defined the carrier' of CA -valued Element of bool [: the carrier of CA, the carrier' of CA:]
[: the carrier of CA, the carrier' of CA:] is non empty Relation-like set
bool [: the carrier of CA, the carrier' of CA:] is non empty set
the T-S_Arcs of CA is non empty Relation-like the carrier' of CA -defined the carrier of CA -valued Element of bool [: the carrier' of CA, the carrier of CA:]
[: the carrier' of CA, the carrier of CA:] is non empty Relation-like set
bool [: the carrier' of CA, the carrier of CA:] is non empty set
the of CA is non empty finite set
the of CA is Relation-like Function-like set
CB is non empty non void V49() with_S-T_arc with_T-S_arc () () ()
the carrier of CB is non empty set
the carrier' of CB is non empty set
the S-T_Arcs of CB is non empty Relation-like the carrier of CB -defined the carrier' of CB -valued Element of bool [: the carrier of CB, the carrier' of CB:]
[: the carrier of CB, the carrier' of CB:] is non empty Relation-like set
bool [: the carrier of CB, the carrier' of CB:] is non empty set
the T-S_Arcs of CB is non empty Relation-like the carrier' of CB -defined the carrier of CB -valued Element of bool [: the carrier' of CB, the carrier of CB:]
[: the carrier' of CB, the carrier of CB:] is non empty Relation-like set
bool [: the carrier' of CB, the carrier of CB:] is non empty set
the of CB is non empty finite set
the of CB is Relation-like Function-like set
O12A is Relation-like (CPNT1) -defined the carrier of CPNT2 -valued Function-like total quasi_total Element of bool [:(CPNT1), the carrier of CPNT2:]
O21A is Relation-like (CPNT2) -defined the carrier of CPNT1 -valued Function-like total quasi_total Element of bool [:(CPNT2), the carrier of CPNT1:]
[O12A,O21A] 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
{O12A,O21A} is non empty functional finite set
{O12A} is non empty trivial functional finite set
{{O12A,O21A},{O12A}} is non empty finite V32() set
q12A is Relation-like Function-like set
dom q12A is set
q21A is Relation-like Function-like set
dom q21A is set
[q12A,q21A] is non empty set
{q12A,q21A} is non empty functional finite set
{q12A} is non empty trivial functional finite set
{{q12A,q21A},{q12A}} is non empty finite V32() set
( the T-S_Arcs of CPNT1 \/ the T-S_Arcs of CPNT2) \/ O12A is non empty Relation-like set
(( the T-S_Arcs of CPNT1 \/ the T-S_Arcs of CPNT2) \/ O12A) \/ O21A is non empty Relation-like set
( the of CPNT1 +* the of CPNT2) +* q12A is Relation-like Function-like set
(( the of CPNT1 +* the of CPNT2) +* q12A) +* q21A is Relation-like Function-like set
O12A is Relation-like (CPNT1) -defined the carrier of CPNT2 -valued Function-like total quasi_total Element of bool [:(CPNT1), the carrier of CPNT2:]
O21A is Relation-like (CPNT2) -defined the carrier of CPNT1 -valued Function-like total quasi_total Element of bool [:(CPNT2), the carrier of CPNT1:]
[O12A,O21A] 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
{O12A,O21A} is non empty functional finite set
{O12A} is non empty trivial functional finite set
{{O12A,O21A},{O12A}} is non empty finite V32() set
q12A is Relation-like Function-like set
dom q12A is set
q21A is Relation-like Function-like set
dom q21A is set
[q12A,q21A] is non empty set
{q12A,q21A} is non empty functional finite set
{q12A} is non empty trivial functional finite set
{{q12A,q21A},{q12A}} is non empty finite V32() set
( the T-S_Arcs of CPNT1 \/ the T-S_Arcs of CPNT2) \/ O12A is non empty Relation-like set
(( the T-S_Arcs of CPNT1 \/ the T-S_Arcs of CPNT2) \/ O12A) \/ O21A is non empty Relation-like set
( the of CPNT1 +* the of CPNT2) +* q12A is Relation-like Function-like set
(( the of CPNT1 +* the of CPNT2) +* q12A) +* q21A is Relation-like Function-like set
O12B is Relation-like (CPNT1) -defined the carrier of CPNT2 -valued Function-like total quasi_total Element of bool [:(CPNT1), the carrier of CPNT2:]
O21B is Relation-like (CPNT2) -defined the carrier of CPNT1 -valued Function-like total quasi_total Element of bool [:(CPNT2), the carrier of CPNT1:]
[O12B,O21B] is non empty Element of [:(bool [:(CPNT1), the carrier of CPNT2:]),(bool [:(CPNT2), the carrier of CPNT1:]):]
{O12B,O21B} is non empty functional finite set
{O12B} is non empty trivial functional finite set
{{O12B,O21B},{O12B}} is non empty finite V32() set
q12B is Relation-like Function-like set
dom q12B is set
q21B is Relation-like Function-like set
dom q21B is set
[q12B,q21B] is non empty set
{q12B,q21B} is non empty functional finite set
{q12B} is non empty trivial functional finite set
{{q12B,q21B},{q12B}} is non empty finite V32() set
( the T-S_Arcs of CPNT1 \/ the T-S_Arcs of CPNT2) \/ O12B is non empty Relation-like set
(( the T-S_Arcs of CPNT1 \/ the T-S_Arcs of CPNT2) \/ O12B) \/ O21B is non empty Relation-like set
( the of CPNT1 +* the of CPNT2) +* q12B is Relation-like Function-like set
(( the of CPNT1 +* the of CPNT2) +* q12B) +* q21B is Relation-like Function-like set
O12B is Relation-like (CPNT1) -defined the carrier of CPNT2 -valued Function-like total quasi_total Element of bool [:(CPNT1), the carrier of CPNT2:]
O21B is Relation-like (CPNT2) -defined the carrier of CPNT1 -valued Function-like total quasi_total Element of bool [:(CPNT2), the carrier of CPNT1:]
[O12B,O21B] is non empty Element of [:(bool [:(CPNT1), the carrier of CPNT2:]),(bool [:(CPNT2), the carrier of CPNT1:]):]
{O12B,O21B} is non empty functional finite set
{O12B} is non empty trivial functional finite set
{{O12B,O21B},{O12B}} is non empty finite V32() set
q12B is Relation-like Function-like set
dom q12B is set
q21B is Relation-like Function-like set
dom q21B is set
[q12B,q21B] is non empty set
{q12B,q21B} is non empty functional finite set
{q12B} is non empty trivial functional finite set
{{q12B,q21B},{q12B}} is non empty finite V32() set
( the T-S_Arcs of CPNT1 \/ the T-S_Arcs of CPNT2) \/ O12B is non empty Relation-like set
(( the T-S_Arcs of CPNT1 \/ the T-S_Arcs of CPNT2) \/ O12B) \/ O21B is non empty Relation-like set
( the of CPNT1 +* the of CPNT2) +* q12B is Relation-like Function-like set
(( the of CPNT1 +* the of CPNT2) +* q12B) +* q21B is Relation-like Function-like set