:: PARSP_1 semantic presentation

K122() is Element of bool K118()
K118() is set
bool K118() is non empty set
K117() is set
bool K117() is non empty set
bool K122() is non empty set
{} is empty set
1 is non empty set
PS is non empty right_complementable add-associative right_zeroed addLoopStr
the carrier of PS is non empty set
a is Element of the carrier of PS
b is Element of the carrier of PS
a - b is Element of the carrier of PS
- (a - b) is Element of the carrier of PS
b - a is Element of the carrier of PS
- a is Element of the carrier of PS
b + (- a) is Element of the carrier of PS
PS is non empty non degenerated non trivial right_complementable almost_left_invertible V92() associative commutative right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed doubleLoopStr
the carrier of PS is non empty non trivial set
0. PS is V49(PS) Element of the carrier of PS
the ZeroF of PS is Element of the carrier of PS
a is Element of the carrier of PS
b is Element of the carrier of PS
a - b is Element of the carrier of PS
b - a is Element of the carrier of PS
c is Element of the carrier of PS
p is Element of the carrier of PS
c - p is Element of the carrier of PS
(a - b) * (c - p) is Element of the carrier of PS
p - c is Element of the carrier of PS
(b - a) * (p - c) is Element of the carrier of PS
((a - b) * (c - p)) - ((b - a) * (p - c)) is Element of the carrier of PS
- (a - b) is Element of the carrier of PS
- (c - p) is Element of the carrier of PS
((a - b) * (c - p)) - ((a - b) * (c - p)) is Element of the carrier of PS
PS is non empty non degenerated non trivial right_complementable almost_left_invertible V92() associative commutative right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed doubleLoopStr
the carrier of PS is non empty non trivial set
0. PS is V49(PS) Element of the carrier of PS
the ZeroF of PS is Element of the carrier of PS
a is Element of the carrier of PS
b is Element of the carrier of PS
b - b is Element of the carrier of PS
a * (b - b) is Element of the carrier of PS
c is Element of the carrier of PS
c - c is Element of the carrier of PS
p is Element of the carrier of PS
(c - c) * p is Element of the carrier of PS
(a * (b - b)) - ((c - c) * p) is Element of the carrier of PS
PS is non empty non degenerated non trivial right_complementable almost_left_invertible V92() associative commutative right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed doubleLoopStr
the carrier of PS is non empty non trivial set
0. PS is V49(PS) Element of the carrier of PS
the ZeroF of PS is Element of the carrier of PS
a is Element of the carrier of PS
b is Element of the carrier of PS
a * b is Element of the carrier of PS
c is Element of the carrier of PS
p is Element of the carrier of PS
c * p is Element of the carrier of PS
(a * b) - (c * p) is Element of the carrier of PS
q is Element of the carrier of PS
a * q is Element of the carrier of PS
c * q is Element of the carrier of PS
s is Element of the carrier of PS
s * p is Element of the carrier of PS
(a * q) - (s * p) is Element of the carrier of PS
s * b is Element of the carrier of PS
(c * q) - (s * b) is Element of the carrier of PS
a " is Element of the carrier of PS
(s * p) * (a ") is Element of the carrier of PS
p * (a ") is Element of the carrier of PS
s * (p * (a ")) is Element of the carrier of PS
c * s is Element of the carrier of PS
(c * s) * (p * (a ")) is Element of the carrier of PS
(c * p) * (a ") is Element of the carrier of PS
c * (p * (a ")) is Element of the carrier of PS
s * c is Element of the carrier of PS
(s * c) * (p * (a ")) is Element of the carrier of PS
PS is non empty non degenerated non trivial right_complementable almost_left_invertible V92() associative commutative right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed doubleLoopStr
the carrier of PS is non empty non trivial set
0. PS is V49(PS) Element of the carrier of PS
the ZeroF of PS is Element of the carrier of PS
a is Element of the carrier of PS
b is Element of the carrier of PS
a * b is Element of the carrier of PS
b * a is Element of the carrier of PS
c is Element of the carrier of PS
p is Element of the carrier of PS
c * p is Element of the carrier of PS
(a * b) - (c * p) is Element of the carrier of PS
p * c is Element of the carrier of PS
(p * c) - (b * a) is Element of the carrier of PS
- ((a * b) - (c * p)) is Element of the carrier of PS
- (b * a) is Element of the carrier of PS
(p * c) + (- (b * a)) is Element of the carrier of PS
PS is non empty non degenerated non trivial right_complementable almost_left_invertible V92() associative commutative right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed doubleLoopStr
the carrier of PS is non empty non trivial set
0. PS is V49(PS) Element of the carrier of PS
the ZeroF of PS is Element of the carrier of PS
a is Element of the carrier of PS
b is Element of the carrier of PS
c is Element of the carrier of PS
b * c is Element of the carrier of PS
p is Element of the carrier of PS
p * a is Element of the carrier of PS
(b * c) - (p * a) is Element of the carrier of PS
q is Element of the carrier of PS
b * q is Element of the carrier of PS
p * q is Element of the carrier of PS
s is Element of the carrier of PS
s * a is Element of the carrier of PS
(b * q) - (s * a) is Element of the carrier of PS
s * c is Element of the carrier of PS
(p * q) - (s * c) is Element of the carrier of PS
a * p is Element of the carrier of PS
c * b is Element of the carrier of PS
(a * p) - (c * b) is Element of the carrier of PS
a * s is Element of the carrier of PS
q * b is Element of the carrier of PS
(a * s) - (q * b) is Element of the carrier of PS
c * s is Element of the carrier of PS
q * p is Element of the carrier of PS
(c * s) - (q * p) is Element of the carrier of PS
PS is non empty non degenerated non trivial right_complementable almost_left_invertible V92() associative commutative right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed doubleLoopStr
the carrier of PS is non empty non trivial set
a is Element of the carrier of PS
b is Element of the carrier of PS
a * b is Element of the carrier of PS
c is Element of the carrier of PS
c * a is Element of the carrier of PS
(c * a) * b is Element of the carrier of PS
p is Element of the carrier of PS
c * p is Element of the carrier of PS
(a * b) * (c * p) is Element of the carrier of PS
((c * a) * b) * p is Element of the carrier of PS
c * (a * b) is Element of the carrier of PS
(c * (a * b)) * p is Element of the carrier of PS
PS is non empty non degenerated non trivial right_complementable almost_left_invertible V92() associative commutative right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed doubleLoopStr
the carrier of PS is non empty non trivial set
0. PS is V49(PS) Element of the carrier of PS
the ZeroF of PS is Element of the carrier of PS
a is Element of the carrier of PS
b is Element of the carrier of PS
a * b is Element of the carrier of PS
c is Element of the carrier of PS
p is Element of the carrier of PS
c * p is Element of the carrier of PS
(a * b) - (c * p) is Element of the carrier of PS
q is Element of the carrier of PS
a * q is Element of the carrier of PS
c * q is Element of the carrier of PS
s is Element of the carrier of PS
(a * q) * s is Element of the carrier of PS
((a * q) * s) * b is Element of the carrier of PS
(c * q) * s is Element of the carrier of PS
((c * q) * s) * p is Element of the carrier of PS
(((a * q) * s) * b) - (((c * q) * s) * p) is Element of the carrier of PS
q * s is Element of the carrier of PS
(q * s) * (a * b) is Element of the carrier of PS
(q * s) * (c * p) is Element of the carrier of PS
(q * s) * ((a * b) - (c * p)) is Element of the carrier of PS
PS is non empty non degenerated non trivial right_complementable almost_left_invertible V92() associative commutative right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed doubleLoopStr
the carrier of PS is non empty non trivial set
a is Element of the carrier of PS
b is Element of the carrier of PS
a - b is Element of the carrier of PS
c is Element of the carrier of PS
a * c is Element of the carrier of PS
p is Element of the carrier of PS
c - p is Element of the carrier of PS
(a - b) * (c - p) is Element of the carrier of PS
a * p is Element of the carrier of PS
- (a * p) is Element of the carrier of PS
b * (c - p) is Element of the carrier of PS
- (b * (c - p)) is Element of the carrier of PS
(- (a * p)) + (- (b * (c - p))) is Element of the carrier of PS
(a * c) + ((- (a * p)) + (- (b * (c - p)))) is Element of the carrier of PS
- b is Element of the carrier of PS
a + (- b) is Element of the carrier of PS
(a + (- b)) * (c - p) is Element of the carrier of PS
a * (c - p) is Element of the carrier of PS
(- b) * (c - p) is Element of the carrier of PS
(a * (c - p)) + ((- b) * (c - p)) is Element of the carrier of PS
(a * (c - p)) + (- (b * (c - p))) is Element of the carrier of PS
(a * c) - (a * p) is Element of the carrier of PS
((a * c) - (a * p)) + (- (b * (c - p))) is Element of the carrier of PS
(a * c) + (- (a * p)) is Element of the carrier of PS
((a * c) + (- (a * p))) + (- (b * (c - p))) is Element of the carrier of PS
PS is non empty non degenerated non trivial right_complementable almost_left_invertible V92() associative commutative right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed doubleLoopStr
the carrier of PS is non empty non trivial set
a is Element of the carrier of PS
b is Element of the carrier of PS
a + b is Element of the carrier of PS
c is Element of the carrier of PS
b + c is Element of the carrier of PS
a + (b + c) is Element of the carrier of PS
p is Element of the carrier of PS
c + p is Element of the carrier of PS
(a + b) + (c + p) is Element of the carrier of PS
(a + (b + c)) + p is Element of the carrier of PS
(a + b) + c is Element of the carrier of PS
((a + b) + c) + p is Element of the carrier of PS
PS is non empty right_complementable add-associative right_zeroed addLoopStr
the carrier of PS is non empty set
b is Element of the carrier of PS
a is Element of the carrier of PS
b + a is Element of the carrier of PS
c is Element of the carrier of PS
c + a is Element of the carrier of PS
(b + a) - (c + a) is Element of the carrier of PS
b - c is Element of the carrier of PS
- (c + a) is Element of the carrier of PS
(b + a) + (- (c + a)) is Element of the carrier of PS
- a is Element of the carrier of PS
- c is Element of the carrier of PS
(- a) + (- c) is Element of the carrier of PS
(b + a) + ((- a) + (- c)) is Element of the carrier of PS
(b + a) + (- a) is Element of the carrier of PS
((b + a) + (- a)) + (- c) is Element of the carrier of PS
a + (- a) is Element of the carrier of PS
b + (a + (- a)) is Element of the carrier of PS
(b + (a + (- a))) + (- c) is Element of the carrier of PS
0. PS is V49(PS) Element of the carrier of PS
the ZeroF of PS is Element of the carrier of PS
b + (0. PS) is Element of the carrier of PS
(b + (0. PS)) + (- c) is Element of the carrier of PS
b + (- c) is Element of the carrier of PS
PS is non empty right_complementable add-associative right_zeroed addLoopStr
the carrier of PS is non empty set
a is Element of the carrier of PS
b is Element of the carrier of PS
a + b is Element of the carrier of PS
- b is Element of the carrier of PS
- a is Element of the carrier of PS
(- b) + (- a) is Element of the carrier of PS
- ((- b) + (- a)) is Element of the carrier of PS
- (a + b) is Element of the carrier of PS
- (- (a + b)) is Element of the carrier of PS
PS is non empty non degenerated non trivial right_complementable almost_left_invertible V92() associative commutative right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed doubleLoopStr
the carrier of PS is non empty non trivial set
0. PS is V49(PS) Element of the carrier of PS
the ZeroF of PS is Element of the carrier of PS
a is Element of the carrier of PS
b is Element of the carrier of PS
a - b is Element of the carrier of PS
b - a is Element of the carrier of PS
c is Element of the carrier of PS
p is Element of the carrier of PS
c - p is Element of the carrier of PS
(a - b) * (c - p) is Element of the carrier of PS
q is Element of the carrier of PS
a - q is Element of the carrier of PS
b - q is Element of the carrier of PS
s is Element of the carrier of PS
c - s is Element of the carrier of PS
(a - q) * (c - s) is Element of the carrier of PS
((a - b) * (c - p)) - ((a - q) * (c - s)) is Element of the carrier of PS
s - p is Element of the carrier of PS
(b - a) * (s - p) is Element of the carrier of PS
s - c is Element of the carrier of PS
(b - q) * (s - c) is Element of the carrier of PS
((b - a) * (s - p)) - ((b - q) * (s - c)) is Element of the carrier of PS
a * c is Element of the carrier of PS
a * p is Element of the carrier of PS
- (a * p) is Element of the carrier of PS
b * (c - p) is Element of the carrier of PS
- (b * (c - p)) is Element of the carrier of PS
(- (a * p)) + (- (b * (c - p))) is Element of the carrier of PS
(a * c) + ((- (a * p)) + (- (b * (c - p)))) is Element of the carrier of PS
a * s is Element of the carrier of PS
- (a * s) is Element of the carrier of PS
q * (c - s) is Element of the carrier of PS
- (q * (c - s)) is Element of the carrier of PS
(- (a * s)) + (- (q * (c - s))) is Element of the carrier of PS
(a * c) + ((- (a * s)) + (- (q * (c - s)))) is Element of the carrier of PS
b * s is Element of the carrier of PS
b * p is Element of the carrier of PS
- (b * p) is Element of the carrier of PS
a * (s - p) is Element of the carrier of PS
- (a * (s - p)) is Element of the carrier of PS
(- (b * p)) + (- (a * (s - p))) is Element of the carrier of PS
(b * s) + ((- (b * p)) + (- (a * (s - p)))) is Element of the carrier of PS
b * c is Element of the carrier of PS
- (b * c) is Element of the carrier of PS
q * (s - c) is Element of the carrier of PS
- (q * (s - c)) is Element of the carrier of PS
(- (b * c)) + (- (q * (s - c))) is Element of the carrier of PS
(b * s) + ((- (b * c)) + (- (q * (s - c)))) is Element of the carrier of PS
((- (b * p)) + (- (a * (s - p)))) - ((- (b * c)) + (- (q * (s - c)))) is Element of the carrier of PS
(a * s) - (a * p) is Element of the carrier of PS
- ((a * s) - (a * p)) is Element of the carrier of PS
(- (b * p)) + (- ((a * s) - (a * p))) is Element of the carrier of PS
((- (b * p)) + (- ((a * s) - (a * p)))) - ((- (b * c)) + (- (q * (s - c)))) is Element of the carrier of PS
(- (a * s)) + (a * p) is Element of the carrier of PS
(- (b * p)) + ((- (a * s)) + (a * p)) is Element of the carrier of PS
((- (b * p)) + ((- (a * s)) + (a * p))) - ((- (b * c)) + (- (q * (s - c)))) is Element of the carrier of PS
(- (b * p)) + (a * p) is Element of the carrier of PS
((- (b * p)) + (a * p)) + (- (a * s)) is Element of the carrier of PS
(((- (b * p)) + (a * p)) + (- (a * s))) - ((- (b * c)) + (- (q * (s - c)))) is Element of the carrier of PS
(a * p) + (- (b * p)) is Element of the carrier of PS
((a * p) + (- (b * p))) + (- (a * s)) is Element of the carrier of PS
- ((- (b * c)) + (- (q * (s - c)))) is Element of the carrier of PS
(((a * p) + (- (b * p))) + (- (a * s))) + (- ((- (b * c)) + (- (q * (s - c))))) is Element of the carrier of PS
- (- (b * c)) is Element of the carrier of PS
- (- (q * (s - c))) is Element of the carrier of PS
(- (- (b * c))) + (- (- (q * (s - c)))) is Element of the carrier of PS
(((a * p) + (- (b * p))) + (- (a * s))) + ((- (- (b * c))) + (- (- (q * (s - c))))) is Element of the carrier of PS
(b * c) + (- (- (q * (s - c)))) is Element of the carrier of PS
(((a * p) + (- (b * p))) + (- (a * s))) + ((b * c) + (- (- (q * (s - c))))) is Element of the carrier of PS
(b * c) + (q * (s - c)) is Element of the carrier of PS
(((a * p) + (- (b * p))) + (- (a * s))) + ((b * c) + (q * (s - c))) is Element of the carrier of PS
(- (a * s)) + (b * c) is Element of the carrier of PS
((a * p) + (- (b * p))) + ((- (a * s)) + (b * c)) is Element of the carrier of PS
(((a * p) + (- (b * p))) + ((- (a * s)) + (b * c))) + (q * (s - c)) is Element of the carrier of PS
((a * p) + (- (b * p))) + (b * c) is Element of the carrier of PS
(- (a * s)) + (q * (s - c)) is Element of the carrier of PS
(((a * p) + (- (b * p))) + (b * c)) + ((- (a * s)) + (q * (s - c))) is Element of the carrier of PS
(- (b * p)) + (b * c) is Element of the carrier of PS
(a * p) + ((- (b * p)) + (b * c)) is Element of the carrier of PS
((a * p) + ((- (b * p)) + (b * c))) + ((- (a * s)) + (q * (s - c))) is Element of the carrier of PS
(b * c) - (b * p) is Element of the carrier of PS
(a * p) + ((b * c) - (b * p)) is Element of the carrier of PS
((a * p) + ((b * c) - (b * p))) + ((- (a * s)) + (q * (s - c))) is Element of the carrier of PS
(a * p) + (b * (c - p)) is Element of the carrier of PS
((a * p) + (b * (c - p))) + ((- (a * s)) + (q * (s - c))) is Element of the carrier of PS
- ((- (a * p)) + (- (b * (c - p)))) is Element of the carrier of PS
(- ((- (a * p)) + (- (b * (c - p))))) + ((- (a * s)) + (q * (s - c))) is Element of the carrier of PS
- (- (a * s)) is Element of the carrier of PS
(- (- (a * s))) + (- (q * (s - c))) is Element of the carrier of PS
- ((- (- (a * s))) + (- (q * (s - c)))) is Element of the carrier of PS
(- ((- (a * p)) + (- (b * (c - p))))) + (- ((- (- (a * s))) + (- (q * (s - c))))) is Element of the carrier of PS
(a * s) + (- (q * (s - c))) is Element of the carrier of PS
- ((a * s) + (- (q * (s - c)))) is Element of the carrier of PS
(- ((- (a * p)) + (- (b * (c - p))))) + (- ((a * s) + (- (q * (s - c))))) is Element of the carrier of PS
((- (a * p)) + (- (b * (c - p)))) + ((a * s) + (- (q * (s - c)))) is Element of the carrier of PS
- (((- (a * p)) + (- (b * (c - p)))) + ((a * s) + (- (q * (s - c))))) is Element of the carrier of PS
(- (a * s)) + (- (- (q * (s - c)))) is Element of the carrier of PS
- ((- (a * s)) + (- (- (q * (s - c))))) is Element of the carrier of PS
((- (a * p)) + (- (b * (c - p)))) + (- ((- (a * s)) + (- (- (q * (s - c)))))) is Element of the carrier of PS
- (((- (a * p)) + (- (b * (c - p)))) + (- ((- (a * s)) + (- (- (q * (s - c))))))) is Element of the carrier of PS
((- (a * p)) + (- (b * (c - p)))) - ((- (a * s)) + (- (- (q * (s - c))))) is Element of the carrier of PS
- (((- (a * p)) + (- (b * (c - p)))) - ((- (a * s)) + (- (- (q * (s - c)))))) is Element of the carrier of PS
- (s - c) is Element of the carrier of PS
(- (s - c)) * q is Element of the carrier of PS
- ((- (s - c)) * q) is Element of the carrier of PS
(- (a * s)) + (- ((- (s - c)) * q)) is Element of the carrier of PS
((- (a * p)) + (- (b * (c - p)))) - ((- (a * s)) + (- ((- (s - c)) * q))) is Element of the carrier of PS
- (((- (a * p)) + (- (b * (c - p)))) - ((- (a * s)) + (- ((- (s - c)) * q)))) is Element of the carrier of PS
((- (a * p)) + (- (b * (c - p)))) - ((- (a * s)) + (- (q * (c - s)))) is Element of the carrier of PS
- (((- (a * p)) + (- (b * (c - p)))) - ((- (a * s)) + (- (q * (c - s))))) is Element of the carrier of PS
- (0. PS) is Element of the carrier of PS
PS is non empty non degenerated non trivial right_complementable almost_left_invertible V92() associative commutative right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed doubleLoopStr
the carrier of PS is non empty non trivial set
a is Element of the carrier of PS
b is Element of the carrier of PS
a + b is Element of the carrier of PS
c is Element of the carrier of PS
- c is Element of the carrier of PS
(a + b) + (- c) is Element of the carrier of PS
a - ((a + b) + (- c)) is Element of the carrier of PS
c - b is Element of the carrier of PS
b + (- c) is Element of the carrier of PS
a + (b + (- c)) is Element of the carrier of PS
a - (a + (b + (- c))) is Element of the carrier of PS
b - c is Element of the carrier of PS
a + (b - c) is Element of the carrier of PS
a - (a + (b - c)) is Element of the carrier of PS
- (a + (b - c)) is Element of the carrier of PS
a + (- (a + (b - c))) is Element of the carrier of PS
- a is Element of the carrier of PS
- (b - c) is Element of the carrier of PS
(- a) + (- (b - c)) is Element of the carrier of PS
a + ((- a) + (- (b - c))) is Element of the carrier of PS
a + (- a) is Element of the carrier of PS
(a + (- a)) + (- (b - c)) is Element of the carrier of PS
0. PS is V49(PS) Element of the carrier of PS
the ZeroF of PS is Element of the carrier of PS
(0. PS) + (- (b - c)) is Element of the carrier of PS
PS is non empty non degenerated non trivial right_complementable almost_left_invertible V92() associative commutative right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed doubleLoopStr
the carrier of PS is non empty non trivial set
0. PS is V49(PS) Element of the carrier of PS
the ZeroF of PS is Element of the carrier of PS
a is Element of the carrier of PS
- a is Element of the carrier of PS
b is Element of the carrier of PS
a - b is Element of the carrier of PS
c is Element of the carrier of PS
p is Element of the carrier of PS
c + p is Element of the carrier of PS
q is Element of the carrier of PS
- q is Element of the carrier of PS
(c + p) + (- q) is Element of the carrier of PS
c - ((c + p) + (- q)) is Element of the carrier of PS
(a - b) * (c - ((c + p) + (- q))) is Element of the carrier of PS
q - p is Element of the carrier of PS
s is Element of the carrier of PS
s + b is Element of the carrier of PS
(s + b) + (- a) is Element of the carrier of PS
s - ((s + b) + (- a)) is Element of the carrier of PS
(s - ((s + b) + (- a))) * (q - p) is Element of the carrier of PS
((a - b) * (c - ((c + p) + (- q)))) - ((s - ((s + b) + (- a))) * (q - p)) is Element of the carrier of PS
PS is non empty non degenerated non trivial right_complementable almost_left_invertible V92() associative commutative right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed doubleLoopStr
the carrier of PS is non empty non trivial set
[: the carrier of PS, the carrier of PS, the carrier of PS:] is non empty set
[:[: the carrier of PS, the carrier of PS, the carrier of PS:],[: the carrier of PS, the carrier of PS, the carrier of PS:]:] is non empty set
[:[:[: the carrier of PS, the carrier of PS, the carrier of PS:],[: the carrier of PS, the carrier of PS, the carrier of PS:]:],[: the carrier of PS, the carrier of PS, the carrier of PS:]:] is non empty set
bool [:[:[: the carrier of PS, the carrier of PS, the carrier of PS:],[: the carrier of PS, the carrier of PS, the carrier of PS:]:],[: the carrier of PS, the carrier of PS, the carrier of PS:]:] is non empty set
[:H₁(PS),H₁(PS):] is non empty set
[:[:H₁(PS),H₁(PS):],H₁(PS):] is non empty set
bool [:[:H₁(PS),H₁(PS):],H₁(PS):] is non empty set
a is V6() V18([:H₁(PS),H₁(PS):],H₁(PS)) Element of bool [:[:H₁(PS),H₁(PS):],H₁(PS):]
b is Element of [: the carrier of PS, the carrier of PS, the carrier of PS:]
c is Element of [: the carrier of PS, the carrier of PS, the carrier of PS:]
a . (b,c) is Element of [: the carrier of PS, the carrier of PS, the carrier of PS:]
b `1_3 is Element of the carrier of PS
c `1_3 is Element of the carrier of PS
(b `1_3) + (c `1_3) is Element of the carrier of PS
b `2_3 is Element of the carrier of PS
c `2_3 is Element of the carrier of PS
(b `2_3) + (c `2_3) is Element of the carrier of PS
b `3_3 is Element of the carrier of PS
c `3_3 is Element of the carrier of PS
(b `3_3) + (c `3_3) is Element of the carrier of PS
[((b `1_3) + (c `1_3)),((b `2_3) + (c `2_3)),((b `3_3) + (c `3_3))] is Element of [: the carrier of PS, the carrier of PS, the carrier of PS:]
[:H₁(PS),H₁(PS):] is non empty set
[:[:H₁(PS),H₁(PS):],H₁(PS):] is non empty set
bool [:[:H₁(PS),H₁(PS):],H₁(PS):] is non empty set
a is V6() V18([:H₁(PS),H₁(PS):],H₁(PS)) Element of bool [:[:H₁(PS),H₁(PS):],H₁(PS):]
b is V6() V18([:H₁(PS),H₁(PS):],H₁(PS)) Element of bool [:[:H₁(PS),H₁(PS):],H₁(PS):]
c is Element of [: the carrier of PS, the carrier of PS, the carrier of PS:]
p is Element of [: the carrier of PS, the carrier of PS, the carrier of PS:]
a . (c,p) is Element of [: the carrier of PS, the carrier of PS, the carrier of PS:]
b . (c,p) is Element of [: the carrier of PS, the carrier of PS, the carrier of PS:]
c `1_3 is Element of the carrier of PS
p `1_3 is Element of the carrier of PS
(c `1_3) + (p `1_3) is Element of the carrier of PS
c `2_3 is Element of the carrier of PS
p `2_3 is Element of the carrier of PS
(c `2_3) + (p `2_3) is Element of the carrier of PS
c `3_3 is Element of the carrier of PS
p `3_3 is Element of the carrier of PS
(c `3_3) + (p `3_3) is Element of the carrier of PS
[((c `1_3) + (p `1_3)),((c `2_3) + (p `2_3)),((c `3_3) + (p `3_3))] is Element of [: the carrier of PS, the carrier of PS, the carrier of PS:]
PS is non empty non degenerated non trivial right_complementable almost_left_invertible V92() associative commutative right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed doubleLoopStr
the carrier of PS is non empty non trivial set
[: the carrier of PS, the carrier of PS, the carrier of PS:] is non empty set
(PS) is V6() V18([:[: the carrier of PS, the carrier of PS, the carrier of PS:],[: the carrier of PS, the carrier of PS, the carrier of PS:]:],[: the carrier of PS, the carrier of PS, the carrier of PS:]) Element of bool [:[:[: the carrier of PS, the carrier of PS, the carrier of PS:],[: the carrier of PS, the carrier of PS, the carrier of PS:]:],[: the carrier of PS, the carrier of PS, the carrier of PS:]:]
[:[: the carrier of PS, the carrier of PS, the carrier of PS:],[: the carrier of PS, the carrier of PS, the carrier of PS:]:] is non empty set
[:[:[: the carrier of PS, the carrier of PS, the carrier of PS:],[: the carrier of PS, the carrier of PS, the carrier of PS:]:],[: the carrier of PS, the carrier of PS, the carrier of PS:]:] is non empty set
bool [:[:[: the carrier of PS, the carrier of PS, the carrier of PS:],[: the carrier of PS, the carrier of PS, the carrier of PS:]:],[: the carrier of PS, the carrier of PS, the carrier of PS:]:] is non empty set
a is Element of [: the carrier of PS, the carrier of PS, the carrier of PS:]
b is Element of [: the carrier of PS, the carrier of PS, the carrier of PS:]
(PS) . (a,b) is Element of [: the carrier of PS, the carrier of PS, the carrier of PS:]
PS is non empty non degenerated non trivial right_complementable almost_left_invertible V92() associative commutative right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed doubleLoopStr
the carrier of PS is non empty non trivial set
[: the carrier of PS, the carrier of PS, the carrier of PS:] is non empty set
a is Element of [: the carrier of PS, the carrier of PS, the carrier of PS:]
b is Element of [: the carrier of PS, the carrier of PS, the carrier of PS:]
(PS,a,b) is Element of [: the carrier of PS, the carrier of PS, the carrier of PS:]
(PS) is V6() V18([:[: the carrier of PS, the carrier of PS, the carrier of PS:],[: the carrier of PS, the carrier of PS, the carrier of PS:]:],[: the carrier of PS, the carrier of PS, the carrier of PS:]) Element of bool [:[:[: the carrier of PS, the carrier of PS, the carrier of PS:],[: the carrier of PS, the carrier of PS, the carrier of PS:]:],[: the carrier of PS, the carrier of PS, the carrier of PS:]:]
[:[: the carrier of PS, the carrier of PS, the carrier of PS:],[: the carrier of PS, the carrier of PS, the carrier of PS:]:] is non empty set
[:[:[: the carrier of PS, the carrier of PS, the carrier of PS:],[: the carrier of PS, the carrier of PS, the carrier of PS:]:],[: the carrier of PS, the carrier of PS, the carrier of PS:]:] is non empty set
bool [:[:[: the carrier of PS, the carrier of PS, the carrier of PS:],[: the carrier of PS, the carrier of PS, the carrier of PS:]:],[: the carrier of PS, the carrier of PS, the carrier of PS:]:] is non empty set
(PS) . (a,b) is Element of [: the carrier of PS, the carrier of PS, the carrier of PS:]
a `1_3 is Element of the carrier of PS
b `1_3 is Element of the carrier of PS
(a `1_3) + (b `1_3) is Element of the carrier of PS
a `2_3 is Element of the carrier of PS
b `2_3 is Element of the carrier of PS
(a `2_3) + (b `2_3) is Element of the carrier of PS
a `3_3 is Element of the carrier of PS
b `3_3 is Element of the carrier of PS
(a `3_3) + (b `3_3) is Element of the carrier of PS
[((a `1_3) + (b `1_3)),((a `2_3) + (b `2_3)),((a `3_3) + (b `3_3))] is Element of [: the carrier of PS, the carrier of PS, the carrier of PS:]
PS is non empty non degenerated non trivial right_complementable almost_left_invertible V92() associative commutative right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed doubleLoopStr
the carrier of PS is non empty non trivial set
a is Element of the carrier of PS
b is Element of the carrier of PS
c is Element of the carrier of PS
[a,b,c] is Element of [: the carrier of PS, the carrier of PS, the carrier of PS:]
[: the carrier of PS, the carrier of PS, the carrier of PS:] is non empty set
p is Element of the carrier of PS
a + p is Element of the carrier of PS
q is Element of the carrier of PS
b + q is Element of the carrier of PS
s is Element of the carrier of PS
[p,q,s] is Element of [: the carrier of PS, the carrier of PS, the carrier of PS:]
(PS,[a,b,c],[p,q,s]) is Element of [: the carrier of PS, the carrier of PS, the carrier of PS:]
(PS) is V6() V18([:[: the carrier of PS, the carrier of PS, the carrier of PS:],[: the carrier of PS, the carrier of PS, the carrier of PS:]:],[: the carrier of PS, the carrier of PS, the carrier of PS:]) Element of bool [:[:[: the carrier of PS, the carrier of PS, the carrier of PS:],[: the carrier of PS, the carrier of PS, the carrier of PS:]:],[: the carrier of PS, the carrier of PS, the carrier of PS:]:]
[:[: the carrier of PS, the carrier of PS, the carrier of PS:],[: the carrier of PS, the carrier of PS, the carrier of PS:]:] is non empty set
[:[:[: the carrier of PS, the carrier of PS, the carrier of PS:],[: the carrier of PS, the carrier of PS, the carrier of PS:]:],[: the carrier of PS, the carrier of PS, the carrier of PS:]:] is non empty set
bool [:[:[: the carrier of PS, the carrier of PS, the carrier of PS:],[: the carrier of PS, the carrier of PS, the carrier of PS:]:],[: the carrier of PS, the carrier of PS, the carrier of PS:]:] is non empty set
(PS) . ([a,b,c],[p,q,s]) is Element of [: the carrier of PS, the carrier of PS, the carrier of PS:]
c + s is Element of the carrier of PS
[(a + p),(b + q),(c + s)] is Element of [: the carrier of PS, the carrier of PS, the carrier of PS:]
[a,b,c] `3_3 is Element of the carrier of PS
[p,q,s] `1_3 is Element of the carrier of PS
[p,q,s] `2_3 is Element of the carrier of PS
[p,q,s] `3_3 is Element of the carrier of PS
[a,b,c] `1_3 is Element of the carrier of PS
[a,b,c] `2_3 is Element of the carrier of PS
PS is non empty non degenerated non trivial right_complementable almost_left_invertible V92() associative commutative right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed doubleLoopStr
the carrier of PS is non empty non trivial set
[: the carrier of PS, the carrier of PS, the carrier of PS:] is non empty set
[:[: the carrier of PS, the carrier of PS, the carrier of PS:],[: the carrier of PS, the carrier of PS, the carrier of PS:]:] is non empty set
bool [:[: the carrier of PS, the carrier of PS, the carrier of PS:],[: the carrier of PS, the carrier of PS, the carrier of PS:]:] is non empty set
[:H₁(PS),H₁(PS):] is non empty set
bool [:H₁(PS),H₁(PS):] is non empty set
a is V6() V18(H₁(PS),H₁(PS)) Element of bool [:H₁(PS),H₁(PS):]
b is Element of [: the carrier of PS, the carrier of PS, the carrier of PS:]
a . b is Element of [: the carrier of PS, the carrier of PS, the carrier of PS:]
b `1_3 is Element of the carrier of PS
- (b `1_3) is Element of the carrier of PS
b `2_3 is Element of the carrier of PS
- (b `2_3) is Element of the carrier of PS
b `3_3 is Element of the carrier of PS
- (b `3_3) is Element of the carrier of PS
[(- (b `1_3)),(- (b `2_3)),(- (b `3_3))] is Element of [: the carrier of PS, the carrier of PS, the carrier of PS:]
[:H₁(PS),H₁(PS):] is non empty set
bool [:H₁(PS),H₁(PS):] is non empty set
a is V6() V18(H₁(PS),H₁(PS)) Element of bool [:H₁(PS),H₁(PS):]
b is V6() V18(H₁(PS),H₁(PS)) Element of bool [:H₁(PS),H₁(PS):]
c is Element of [: the carrier of PS, the carrier of PS, the carrier of PS:]
a . c is Element of H₁(PS)
b . c is Element of H₁(PS)
c `1_3 is Element of the carrier of PS
- (c `1_3) is Element of the carrier of PS
c `2_3 is Element of the carrier of PS
- (c `2_3) is Element of the carrier of PS
c `3_3 is Element of the carrier of PS
- (c `3_3) is Element of the carrier of PS
[(- (c `1_3)),(- (c `2_3)),(- (c `3_3))] is Element of [: the carrier of PS, the carrier of PS, the carrier of PS:]
PS is non empty non degenerated non trivial right_complementable almost_left_invertible V92() associative commutative right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed doubleLoopStr
the carrier of PS is non empty non trivial set
[: the carrier of PS, the carrier of PS, the carrier of PS:] is non empty set
(PS) is V6() V18([: the carrier of PS, the carrier of PS, the carrier of PS:],[: the carrier of PS, the carrier of PS, the carrier of PS:]) Element of bool [:[: the carrier of PS, the carrier of PS, the carrier of PS:],[: the carrier of PS, the carrier of PS, the carrier of PS:]:]
[:[: the carrier of PS, the carrier of PS, the carrier of PS:],[: the carrier of PS, the carrier of PS, the carrier of PS:]:] is non empty set
bool [:[: the carrier of PS, the carrier of PS, the carrier of PS:],[: the carrier of PS, the carrier of PS, the carrier of PS:]:] is non empty set
a is Element of [: the carrier of PS, the carrier of PS, the carrier of PS:]
(PS) . a is Element of [: the carrier of PS, the carrier of PS, the carrier of PS:]
PS is non empty non degenerated non trivial right_complementable almost_left_invertible V92() associative commutative right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed doubleLoopStr
the carrier of PS is non empty non trivial set
[: the carrier of PS, the carrier of PS, the carrier of PS:] is non empty set
a is Element of [: the carrier of PS, the carrier of PS, the carrier of PS:]
(PS,a) is Element of [: the carrier of PS, the carrier of PS, the carrier of PS:]
(PS) is V6() V18([: the carrier of PS, the carrier of PS, the carrier of PS:],[: the carrier of PS, the carrier of PS, the carrier of PS:]) Element of bool [:[: the carrier of PS, the carrier of PS, the carrier of PS:],[: the carrier of PS, the carrier of PS, the carrier of PS:]:]
[:[: the carrier of PS, the carrier of PS, the carrier of PS:],[: the carrier of PS, the carrier of PS, the carrier of PS:]:] is non empty set
bool [:[: the carrier of PS, the carrier of PS, the carrier of PS:],[: the carrier of PS, the carrier of PS, the carrier of PS:]:] is non empty set
(PS) . a is Element of [: the carrier of PS, the carrier of PS, the carrier of PS:]
a `1_3 is Element of the carrier of PS
- (a `1_3) is Element of the carrier of PS
a `2_3 is Element of the carrier of PS
- (a `2_3) is Element of the carrier of PS
a `3_3 is Element of the carrier of PS
- (a `3_3) is Element of the carrier of PS
[(- (a `1_3)),(- (a `2_3)),(- (a `3_3))] is Element of [: the carrier of PS, the carrier of PS, the carrier of PS:]
PS is set
[:PS,PS,PS,PS:] is set
the non empty set is non empty set
the ( the non empty set ) is ( the non empty set )
( the non empty set , the ( the non empty set )) is () ()
the carrier of ( the non empty set , the ( the non empty set )) is set
PS is non empty ()
the carrier of PS is non empty set
PS is non empty non degenerated non trivial right_complementable almost_left_invertible V92() associative commutative right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed doubleLoopStr
the carrier of PS is non empty non trivial set
[: the carrier of PS, the carrier of PS, the carrier of PS:] is non empty set
PS is non empty non degenerated non trivial right_complementable almost_left_invertible V92() associative commutative right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed doubleLoopStr
(PS) is set
the carrier of PS is non empty non trivial set
[: the carrier of PS, the carrier of PS, the carrier of PS:] is non empty set
PS is non empty non degenerated non trivial right_complementable almost_left_invertible V92() associative commutative right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed doubleLoopStr
(PS) is non empty set
the carrier of PS is non empty non trivial set
[: the carrier of PS, the carrier of PS, the carrier of PS:] is non empty set
[:(PS),(PS),(PS),(PS):] is non empty set
PS is non empty non degenerated non trivial right_complementable almost_left_invertible V92() associative commutative right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed doubleLoopStr
(PS) is set
(PS) is non empty set
the carrier of PS is non empty non trivial set
[: the carrier of PS, the carrier of PS, the carrier of PS:] is non empty set
[:(PS),(PS),(PS),(PS):] is non empty set
PS is non empty non degenerated non trivial right_complementable almost_left_invertible V92() associative commutative right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed doubleLoopStr
(PS) is non empty set
(PS) is non empty set
the carrier of PS is non empty non trivial set
[: the carrier of PS, the carrier of PS, the carrier of PS:] is non empty set
[:(PS),(PS),(PS),(PS):] is non empty set
0. PS is V49(PS) Element of the carrier of PS
the ZeroF of PS is Element of the carrier of PS
a is set
b is set
c is set
p is Element of [: the carrier of PS, the carrier of PS, the carrier of PS:]
q is Element of [: the carrier of PS, the carrier of PS, the carrier of PS:]
s is Element of [: the carrier of PS, the carrier of PS, the carrier of PS:]
s is Element of [: the carrier of PS, the carrier of PS, the carrier of PS:]
[p,q,s,s] is Element of [:[: the carrier of PS, the carrier of PS, the carrier of PS:],[: the carrier of PS, the carrier of PS, the carrier of PS:],[: the carrier of PS, the carrier of PS, the carrier of PS:],[: the carrier of PS, the carrier of PS, the carrier of PS:]:]
[:[: the carrier of PS, the carrier of PS, the carrier of PS:],[: the carrier of PS, the carrier of PS, the carrier of PS:],[: the carrier of PS, the carrier of PS, the carrier of PS:],[: the carrier of PS, the carrier of PS, the carrier of PS:]:] is non empty set
p `1_3 is Element of the carrier of PS
q `1_3 is Element of the carrier of PS
(p `1_3) - (q `1_3) is Element of the carrier of PS
s `2_3 is Element of the carrier of PS
s `2_3 is Element of the carrier of PS
(s `2_3) - (s `2_3) is Element of the carrier of PS
((p `1_3) - (q `1_3)) * ((s `2_3) - (s `2_3)) is Element of the carrier of PS
s `1_3 is Element of the carrier of PS
s `1_3 is Element of the carrier of PS
(s `1_3) - (s `1_3) is Element of the carrier of PS
p `2_3 is Element of the carrier of PS
q `2_3 is Element of the carrier of PS
(p `2_3) - (q `2_3) is Element of the carrier of PS
((s `1_3) - (s `1_3)) * ((p `2_3) - (q `2_3)) is Element of the carrier of PS
(((p `1_3) - (q `1_3)) * ((s `2_3) - (s `2_3))) - (((s `1_3) - (s `1_3)) * ((p `2_3) - (q `2_3))) is Element of the carrier of PS
s `3_3 is Element of the carrier of PS
s `3_3 is Element of the carrier of PS
(s `3_3) - (s `3_3) is Element of the carrier of PS
((p `1_3) - (q `1_3)) * ((s `3_3) - (s `3_3)) is Element of the carrier of PS
p `3_3 is Element of the carrier of PS
q `3_3 is Element of the carrier of PS
(p `3_3) - (q `3_3) is Element of the carrier of PS
((s `1_3) - (s `1_3)) * ((p `3_3) - (q `3_3)) is Element of the carrier of PS
(((p `1_3) - (q `1_3)) * ((s `3_3) - (s `3_3))) - (((s `1_3) - (s `1_3)) * ((p `3_3) - (q `3_3))) is Element of the carrier of PS
((p `2_3) - (q `2_3)) * ((s `3_3) - (s `3_3)) is Element of the carrier of PS
((s `2_3) - (s `2_3)) * ((p `3_3) - (q `3_3)) is Element of the carrier of PS
(((p `2_3) - (q `2_3)) * ((s `3_3) - (s `3_3))) - (((s `2_3) - (s `2_3)) * ((p `3_3) - (q `3_3))) is Element of the carrier of PS
p is Element of [: the carrier of PS, the carrier of PS, the carrier of PS:]
q is Element of [: the carrier of PS, the carrier of PS, the carrier of PS:]
s is Element of [: the carrier of PS, the carrier of PS, the carrier of PS:]
s is Element of [: the carrier of PS, the carrier of PS, the carrier of PS:]
[p,q,s,s] is Element of [:[: the carrier of PS, the carrier of PS, the carrier of PS:],[: the carrier of PS, the carrier of PS, the carrier of PS:],[: the carrier of PS, the carrier of PS, the carrier of PS:],[: the carrier of PS, the carrier of PS, the carrier of PS:]:]
[:[: the carrier of PS, the carrier of PS, the carrier of PS:],[: the carrier of PS, the carrier of PS, the carrier of PS:],[: the carrier of PS, the carrier of PS, the carrier of PS:],[: the carrier of PS, the carrier of PS, the carrier of PS:]:] is non empty set
p `1_3 is Element of the carrier of PS
q `1_3 is Element of the carrier of PS
(p `1_3) - (q `1_3) is Element of the carrier of PS
s `2_3 is Element of the carrier of PS
s `2_3 is Element of the carrier of PS
(s `2_3) - (s `2_3) is Element of the carrier of PS
((p `1_3) - (q `1_3)) * ((s `2_3) - (s `2_3)) is Element of the carrier of PS
s `1_3 is Element of the carrier of PS
s `1_3 is Element of the carrier of PS
(s `1_3) - (s `1_3) is Element of the carrier of PS
p `2_3 is Element of the carrier of PS
q `2_3 is Element of the carrier of PS
(p `2_3) - (q `2_3) is Element of the carrier of PS
((s `1_3) - (s `1_3)) * ((p `2_3) - (q `2_3)) is Element of the carrier of PS
(((p `1_3) - (q `1_3)) * ((s `2_3) - (s `2_3))) - (((s `1_3) - (s `1_3)) * ((p `2_3) - (q `2_3))) is Element of the carrier of PS
s `3_3 is Element of the carrier of PS
s `3_3 is Element of the carrier of PS
(s `3_3) - (s `3_3) is Element of the carrier of PS
((p `1_3) - (q `1_3)) * ((s `3_3) - (s `3_3)) is Element of the carrier of PS
p `3_3 is Element of the carrier of PS
q `3_3 is Element of the carrier of PS
(p `3_3) - (q `3_3) is Element of the carrier of PS
((s `1_3) - (s `1_3)) * ((p `3_3) - (q `3_3)) is Element of the carrier of PS
(((p `1_3) - (q `1_3)) * ((s `3_3) - (s `3_3))) - (((s `1_3) - (s `1_3)) * ((p `3_3) - (q `3_3))) is Element of the carrier of PS
((p `2_3) - (q `2_3)) * ((s `3_3) - (s `3_3)) is Element of the carrier of PS
((s `2_3) - (s `2_3)) * ((p `3_3) - (q `3_3)) is Element of the carrier of PS
(((p `2_3) - (q `2_3)) * ((s `3_3) - (s `3_3))) - (((s `2_3) - (s `2_3)) * ((p `3_3) - (q `3_3))) is Element of the carrier of PS
PS is non empty non degenerated non trivial right_complementable almost_left_invertible V92() associative commutative right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed doubleLoopStr
(PS) is set
(PS) is non empty set
the carrier of PS is non empty non trivial set
[: the carrier of PS, the carrier of PS, the carrier of PS:] is non empty set
[:(PS),(PS),(PS),(PS):] is non empty set
a is set
(PS) is non empty set
PS is non empty non degenerated non trivial right_complementable almost_left_invertible V92() associative commutative right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed doubleLoopStr
(PS) is set
(PS) is non empty set
the carrier of PS is non empty non trivial set
[: the carrier of PS, the carrier of PS, the carrier of PS:] is non empty set
[:(PS),(PS),(PS),(PS):] is non empty set
PS is non empty non degenerated non trivial right_complementable almost_left_invertible V92() associative commutative right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed doubleLoopStr
(PS) is non empty set
the carrier of PS is non empty non trivial set
[: the carrier of PS, the carrier of PS, the carrier of PS:] is non empty set
(PS) is ((PS))
(PS) is set
((PS),(PS)) is () ()
PS is non empty non degenerated non trivial right_complementable almost_left_invertible V92() associative commutative right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed doubleLoopStr
(PS) is ()
(PS) is non empty set
the carrier of PS is non empty non trivial set
[: the carrier of PS, the carrier of PS, the carrier of PS:] is non empty set
(PS) is ((PS))
(PS) is set
((PS),(PS)) is () ()
PS is non empty non degenerated non trivial right_complementable almost_left_invertible V92() associative commutative right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed doubleLoopStr
(PS) is non empty () ()
(PS) is non empty set
the carrier of PS is non empty non trivial set
[: the carrier of PS, the carrier of PS, the carrier of PS:] is non empty set
(PS) is ((PS))
(PS) is set
((PS),(PS)) is () ()
the carrier of (PS) is non empty set
PS is non empty non degenerated non trivial right_complementable almost_left_invertible V92() associative commutative right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed doubleLoopStr
(PS) is non empty () ()
(PS) is non empty set
the carrier of PS is non empty non trivial set
[: the carrier of PS, the carrier of PS, the carrier of PS:] is non empty set
(PS) is ((PS))
(PS) is set
((PS),(PS)) is () ()
the of (PS) is ( the carrier of (PS))
the carrier of (PS) is non empty set
PS is non empty non degenerated non trivial right_complementable almost_left_invertible V92() associative commutative right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed doubleLoopStr
(PS) is non empty () ()
(PS) is non empty set
the carrier of PS is non empty non trivial set
[: the carrier of PS, the carrier of PS, the carrier of PS:] is non empty set
(PS) is ((PS))
(PS) is set
((PS),(PS)) is () ()
the carrier of (PS) is non empty set
q is non empty non degenerated non trivial right_complementable almost_left_invertible V92() associative commutative right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed doubleLoopStr
(q) is non empty () ()
(q) is non empty set
the carrier of q is non empty non trivial set
[: the carrier of q, the carrier of q, the carrier of q:] is non empty set
(q) is ((q))
(q) is set
((q),(q)) is () ()
the carrier of (q) is non empty set
a is Element of the carrier of (PS)
b is Element of the carrier of (PS)
c is Element of the carrier of (PS)
p is Element of the carrier of (PS)
[a,b,c,p] is Element of [: the carrier of (PS), the carrier of (PS), the carrier of (PS), the carrier of (PS):]
[: the carrier of (PS), the carrier of (PS), the carrier of (PS), the carrier of (PS):] is non empty set
s is Element of the carrier of (q)
s is Element of the carrier of (q)
s is Element of the carrier of (q)
c₁₀ is Element of the carrier of (q)
[s,s,s,c₁₀] is Element of [: the carrier of (q), the carrier of (q), the carrier of (q), the carrier of (q):]
[: the carrier of (q), the carrier of (q), the carrier of (q), the carrier of (q):] is non empty set
PS is non empty non degenerated non trivial right_complementable almost_left_invertible V92() associative commutative right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed doubleLoopStr
(PS) is non empty () ()
(PS) is non empty set
the carrier of PS is non empty non trivial set
[: the carrier of PS, the carrier of PS, the carrier of PS:] is non empty set
(PS) is ((PS))
(PS) is set
((PS),(PS)) is () ()
the carrier of (PS) is non empty set
q is non empty non degenerated non trivial right_complementable almost_left_invertible V92() associative commutative right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed doubleLoopStr
(q) is non empty () ()
(q) is non empty set
the carrier of q is non empty non trivial set
[: the carrier of q, the carrier of q, the carrier of q:] is non empty set
(q) is ((q))
(q) is set
((q),(q)) is () ()
the carrier of (q) is non empty set
a is Element of the carrier of (PS)
b is Element of the carrier of (PS)
c is Element of the carrier of (PS)
p is Element of the carrier of (PS)
[a,b,c,p] is Element of [: the carrier of (PS), the carrier of (PS), the carrier of (PS), the carrier of (PS):]
[: the carrier of (PS), the carrier of (PS), the carrier of (PS), the carrier of (PS):] is non empty set
(PS) is non empty set
[:(PS),(PS),(PS),(PS):] is non empty set
0. PS is V49(PS) Element of the carrier of PS
the ZeroF of PS is Element of the carrier of PS
s is Element of the carrier of (q)
s is Element of the carrier of (q)
s is Element of the carrier of (q)
c₁₀ is Element of the carrier of (q)
[s,s,s,c₁₀] is Element of [: the carrier of (q), the carrier of (q), the carrier of (q), the carrier of (q):]
[: the carrier of (q), the carrier of (q), the carrier of (q), the carrier of (q):] is non empty set
(q) is non empty set
[:(q),(q),(q),(q):] is non empty set
h is Element of [: the carrier of q, the carrier of q, the carrier of q:]
i is Element of [: the carrier of q, the carrier of q, the carrier of q:]
j is Element of [: the carrier of q, the carrier of q, the carrier of q:]
k is Element of [: the carrier of q, the carrier of q, the carrier of q:]
[h,i,j,k] is Element of [:[: the carrier of q, the carrier of q, the carrier of q:],[: the carrier of q, the carrier of q, the carrier of q:],[: the carrier of q, the carrier of q, the carrier of q:],[: the carrier of q, the carrier of q, the carrier of q:]:]
[:[: the carrier of q, the carrier of q, the carrier of q:],[: the carrier of q, the carrier of q, the carrier of q:],[: the carrier of q, the carrier of q, the carrier of q:],[: the carrier of q, the carrier of q, the carrier of q:]:] is non empty set
h `1_3 is Element of the carrier of q
i `1_3 is Element of the carrier of q
(h `1_3) - (i `1_3) is Element of the carrier of q
j `2_3 is Element of the carrier of q
k `2_3 is Element of the carrier of q
(j `2_3) - (k `2_3) is Element of the carrier of q
((h `1_3) - (i `1_3)) * ((j `2_3) - (k `2_3)) is Element of the carrier of q
j `1_3 is Element of the carrier of q
k `1_3 is Element of the carrier of q
(j `1_3) - (k `1_3) is Element of the carrier of q
h `2_3 is Element of the carrier of q
i `2_3 is Element of the carrier of q
(h `2_3) - (i `2_3) is Element of the carrier of q
((j `1_3) - (k `1_3)) * ((h `2_3) - (i `2_3)) is Element of the carrier of q
(((h `1_3) - (i `1_3)) * ((j `2_3) - (k `2_3))) - (((j `1_3) - (k `1_3)) * ((h `2_3) - (i `2_3))) is Element of the carrier of q
0. q is V49(q) Element of the carrier of q
the ZeroF of q is Element of the carrier of q
j `3_3 is Element of the carrier of q
k `3_3 is Element of the carrier of q
(j `3_3) - (k `3_3) is Element of the carrier of q
((h `1_3) - (i `1_3)) * ((j `3_3) - (k `3_3)) is Element of the carrier of q
h `3_3 is Element of the carrier of q
i `3_3 is Element of the carrier of q
(h `3_3) - (i `3_3) is Element of the carrier of q
((j `1_3) - (k `1_3)) * ((h `3_3) - (i `3_3)) is Element of the carrier of q
(((h `1_3) - (i `1_3)) * ((j `3_3) - (k `3_3))) - (((j `1_3) - (k `1_3)) * ((h `3_3) - (i `3_3))) is Element of the carrier of q
((h `2_3) - (i `2_3)) * ((j `3_3) - (k `3_3)) is Element of the carrier of q
((j `2_3) - (k `2_3)) * ((h `3_3) - (i `3_3)) is Element of the carrier of q
(((h `2_3) - (i `2_3)) * ((j `3_3) - (k `3_3))) - (((j `2_3) - (k `2_3)) * ((h `3_3) - (i `3_3))) is Element of the carrier of q
PS is non empty non degenerated non trivial right_complementable almost_left_invertible V92() associative commutative right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed doubleLoopStr
(PS) is non empty () ()
(PS) is non empty set
the carrier of PS is non empty non trivial set
[: the carrier of PS, the carrier of PS, the carrier of PS:] is non empty set
(PS) is ((PS))
(PS) is set
((PS),(PS)) is () ()
the carrier of (PS) is non empty set
(PS) is non empty set
[:(PS),(PS),(PS),(PS):] is non empty set
0. PS is V49(PS) Element of the carrier of PS
the ZeroF of PS is Element of the carrier of PS
a is Element of the carrier of (PS)
b is Element of the carrier of (PS)
c is Element of the carrier of (PS)
p is Element of the carrier of (PS)
[a,b,c,p] is Element of [: the carrier of (PS), the carrier of (PS), the carrier of (PS), the carrier of (PS):]
[: the carrier of (PS), the carrier of (PS), the carrier of (PS), the carrier of (PS):] is non empty set
q is Element of [: the carrier of PS, the carrier of PS, the carrier of PS:]
s is Element of [: the carrier of PS, the carrier of PS, the carrier of PS:]
s is Element of [: the carrier of PS, the carrier of PS, the carrier of PS:]
s is Element of [: the carrier of PS, the carrier of PS, the carrier of PS:]
[q,s,s,s] is Element of [:[: the carrier of PS, the carrier of PS, the carrier of PS:],[: the carrier of PS, the carrier of PS, the carrier of PS:],[: the carrier of PS, the carrier of PS, the carrier of PS:],[: the carrier of PS, the carrier of PS, the carrier of PS:]:]
[:[: the carrier of PS, the carrier of PS, the carrier of PS:],[: the carrier of PS, the carrier of PS, the carrier of PS:],[: the carrier of PS, the carrier of PS, the carrier of PS:],[: the carrier of PS, the carrier of PS, the carrier of PS:]:] is non empty set
q `1_3 is Element of the carrier of PS
s `1_3 is Element of the carrier of PS
(q `1_3) - (s `1_3) is Element of the carrier of PS
s `2_3 is Element of the carrier of PS
s `2_3 is Element of the carrier of PS
(s `2_3) - (s `2_3) is Element of the carrier of PS
((q `1_3) - (s `1_3)) * ((s `2_3) - (s `2_3)) is Element of the carrier of PS
s `1_3 is Element of the carrier of PS
s `1_3 is Element of the carrier of PS
(s `1_3) - (s `1_3) is Element of the carrier of PS
q `2_3 is Element of the carrier of PS
s `2_3 is Element of the carrier of PS
(q `2_3) - (s `2_3) is Element of the carrier of PS
((s `1_3) - (s `1_3)) * ((q `2_3) - (s `2_3)) is Element of the carrier of PS
(((q `1_3) - (s `1_3)) * ((s `2_3) - (s `2_3))) - (((s `1_3) - (s `1_3)) * ((q `2_3) - (s `2_3))) is Element of the carrier of PS
s `3_3 is Element of the carrier of PS
s `3_3 is Element of the carrier of PS
(s `3_3) - (s `3_3) is Element of the carrier of PS
((q `1_3) - (s `1_3)) * ((s `3_3) - (s `3_3)) is Element of the carrier of PS
q `3_3 is Element of the carrier of PS
s `3_3 is Element of the carrier of PS
(q `3_3) - (s `3_3) is Element of the carrier of PS
((s `1_3) - (s `1_3)) * ((q `3_3) - (s `3_3)) is Element of the carrier of PS
(((q `1_3) - (s `1_3)) * ((s `3_3) - (s `3_3))) - (((s `1_3) - (s `1_3)) * ((q `3_3) - (s `3_3))) is Element of the carrier of PS
((q `2_3) - (s `2_3)) * ((s `3_3) - (s `3_3)) is Element of the carrier of PS
((s `2_3) - (s `2_3)) * ((q `3_3) - (s `3_3)) is Element of the carrier of PS
(((q `2_3) - (s `2_3)) * ((s `3_3) - (s `3_3))) - (((s `2_3) - (s `2_3)) * ((q `3_3) - (s `3_3))) is Element of the carrier of PS
PS is non empty non degenerated non trivial right_complementable almost_left_invertible V92() associative commutative right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed doubleLoopStr
(PS) is non empty () ()
(PS) is non empty set
the carrier of PS is non empty non trivial set
[: the carrier of PS, the carrier of PS, the carrier of PS:] is non empty set
(PS) is ((PS))
(PS) is set
((PS),(PS)) is () ()
the carrier of (PS) is non empty set
PS is non empty non degenerated non trivial right_complementable almost_left_invertible V92() associative commutative right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed doubleLoopStr
(PS) is non empty () ()
(PS) is non empty set
the carrier of PS is non empty non trivial set
[: the carrier of PS, the carrier of PS, the carrier of PS:] is non empty set
(PS) is ((PS))
(PS) is set
((PS),(PS)) is () ()
the carrier of (PS) is non empty set
a is Element of the carrier of (PS)
b is Element of the carrier of (PS)
c is Element of the carrier of (PS)
p is Element of the carrier of (PS)
[a,b,c,p] is Element of [: the carrier of (PS), the carrier of (PS), the carrier of (PS), the carrier of (PS):]
[: the carrier of (PS), the carrier of (PS), the carrier of (PS), the carrier of (PS):] is non empty set
(PS) is non empty set
[:(PS),(PS),(PS),(PS):] is non empty set
PS is non empty non degenerated non trivial right_complementable almost_left_invertible V92() associative commutative right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed doubleLoopStr
(PS) is non empty () ()
(PS) is non empty set
the carrier of PS is non empty non trivial set
[: the carrier of PS, the carrier of PS, the carrier of PS:] is non empty set
(PS) is ((PS))
(PS) is set
((PS),(PS)) is () ()
the carrier of (PS) is non empty set
0. PS is V49(PS) Element of the carrier of PS
the ZeroF of PS is Element of the carrier of PS
a is Element of the carrier of (PS)
b is Element of the carrier of (PS)
c is Element of the carrier of (PS)
p is Element of the carrier of (PS)
[a,b,c,p] is Element of [: the carrier of (PS), the carrier of (PS), the carrier of (PS), the carrier of (PS):]
[: the carrier of (PS), the carrier of (PS), the carrier of (PS), the carrier of (PS):] is non empty set
(PS) is non empty set
[:(PS),(PS),(PS),(PS):] is non empty set
q is Element of [: the carrier of PS, the carrier of PS, the carrier of PS:]
s is Element of [: the carrier of PS, the carrier of PS, the carrier of PS:]
s is Element of [: the carrier of PS, the carrier of PS, the carrier of PS:]
s is Element of [: the carrier of PS, the carrier of PS, the carrier of PS:]
[q,s,s,s] is Element of [:[: the carrier of PS, the carrier of PS, the carrier of PS:],[: the carrier of PS, the carrier of PS, the carrier of PS:],[: the carrier of PS, the carrier of PS, the carrier of PS:],[: the carrier of PS, the carrier of PS, the carrier of PS:]:]
[:[: the carrier of PS, the carrier of PS, the carrier of PS:],[: the carrier of PS, the carrier of PS, the carrier of PS:],[: the carrier of PS, the carrier of PS, the carrier of PS:],[: the carrier of PS, the carrier of PS, the carrier of PS:]:] is non empty set
q `1_3 is Element of the carrier of PS
s `1_3 is Element of the carrier of PS
(q `1_3) - (s `1_3) is Element of the carrier of PS
s `2_3 is Element of the carrier of PS
s `2_3 is Element of the carrier of PS
(s `2_3) - (s `2_3) is Element of the carrier of PS
((q `1_3) - (s `1_3)) * ((s `2_3) - (s `2_3)) is Element of the carrier of PS
s `1_3 is Element of the carrier of PS
s `1_3 is Element of the carrier of PS
(s `1_3) - (s `1_3) is Element of the carrier of PS
q `2_3 is Element of the carrier of PS
s `2_3 is Element of the carrier of PS
(q `2_3) - (s `2_3) is Element of the carrier of PS
((s `1_3) - (s `1_3)) * ((q `2_3) - (s `2_3)) is Element of the carrier of PS
(((q `1_3) - (s `1_3)) * ((s `2_3) - (s `2_3))) - (((s `1_3) - (s `1_3)) * ((q `2_3) - (s `2_3))) is Element of the carrier of PS
s `3_3 is Element of the carrier of PS
s `3_3 is Element of the carrier of PS
(s `3_3) - (s `3_3) is Element of the carrier of PS
((q `1_3) - (s `1_3)) * ((s `3_3) - (s `3_3)) is Element of the carrier of PS
q `3_3 is Element of the carrier of PS
s `3_3 is Element of the carrier of PS
(q `3_3) - (s `3_3) is Element of the carrier of PS
((s `1_3) - (s `1_3)) * ((q `3_3) - (s `3_3)) is Element of the carrier of PS
(((q `1_3) - (s `1_3)) * ((s `3_3) - (s `3_3))) - (((s `1_3) - (s `1_3)) * ((q `3_3) - (s `3_3))) is Element of the carrier of PS
((q `2_3) - (s `2_3)) * ((s `3_3) - (s `3_3)) is Element of the carrier of PS
((s `2_3) - (s `2_3)) * ((q `3_3) - (s `3_3)) is Element of the carrier of PS
(((q `2_3) - (s `2_3)) * ((s `3_3) - (s `3_3))) - (((s `2_3) - (s `2_3)) * ((q `3_3) - (s `3_3))) is Element of the carrier of PS
PS is non empty non degenerated non trivial right_complementable almost_left_invertible V92() associative commutative right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed doubleLoopStr
(PS) is non empty () ()
(PS) is non empty set
the carrier of PS is non empty non trivial set
[: the carrier of PS, the carrier of PS, the carrier of PS:] is non empty set
(PS) is ((PS))
(PS) is set
((PS),(PS)) is () ()
the carrier of (PS) is non empty set
a is Element of the carrier of (PS)
b is Element of the carrier of (PS)
[a,b,b,a] is Element of [: the carrier of (PS), the carrier of (PS), the carrier of (PS), the carrier of (PS):]
[: the carrier of (PS), the carrier of (PS), the carrier of (PS), the carrier of (PS):] is non empty set
c is Element of [: the carrier of PS, the carrier of PS, the carrier of PS:]
p is Element of [: the carrier of PS, the carrier of PS, the carrier of PS:]
[c,p,p,c] is Element of [:[: the carrier of PS, the carrier of PS, the carrier of PS:],[: the carrier of PS, the carrier of PS, the carrier of PS:],[: the carrier of PS, the carrier of PS, the carrier of PS:],[: the carrier of PS, the carrier of PS, the carrier of PS:]:]
[:[: the carrier of PS, the carrier of PS, the carrier of PS:],[: the carrier of PS, the carrier of PS, the carrier of PS:],[: the carrier of PS, the carrier of PS, the carrier of PS:],[: the carrier of PS, the carrier of PS, the carrier of PS:]:] is non empty set
c `2_3 is Element of the carrier of PS
p `2_3 is Element of the carrier of PS
(c `2_3) - (p `2_3) is Element of the carrier of PS
p `3_3 is Element of the carrier of PS
c `3_3 is Element of the carrier of PS
(p `3_3) - (c `3_3) is Element of the carrier of PS
((c `2_3) - (p `2_3)) * ((p `3_3) - (c `3_3)) is Element of the carrier of PS
(p `2_3) - (c `2_3) is Element of the carrier of PS
(c `3_3) - (p `3_3) is Element of the carrier of PS
((p `2_3) - (c `2_3)) * ((c `3_3) - (p `3_3)) is Element of the carrier of PS
(((c `2_3) - (p `2_3)) * ((p `3_3) - (c `3_3))) - (((p `2_3) - (c `2_3)) * ((c `3_3) - (p `3_3))) is Element of the carrier of PS
0. PS is V49(PS) Element of the carrier of PS
the ZeroF of PS is Element of the carrier of PS
c `1_3 is Element of the carrier of PS
p `1_3 is Element of the carrier of PS
(c `1_3) - (p `1_3) is Element of the carrier of PS
((c `1_3) - (p `1_3)) * ((p `2_3) - (c `2_3)) is Element of the carrier of PS
(p `1_3) - (c `1_3) is Element of the carrier of PS
((p `1_3) - (c `1_3)) * ((c `2_3) - (p `2_3)) is Element of the carrier of PS
(((c `1_3) - (p `1_3)) * ((p `2_3) - (c `2_3))) - (((p `1_3) - (c `1_3)) * ((c `2_3) - (p `2_3))) is Element of the carrier of PS
((c `1_3) - (p `1_3)) * ((p `3_3) - (c `3_3)) is Element of the carrier of PS
((p `1_3) - (c `1_3)) * ((c `3_3) - (p `3_3)) is Element of the carrier of PS
(((c `1_3) - (p `1_3)) * ((p `3_3) - (c `3_3))) - (((p `1_3) - (c `1_3)) * ((c `3_3) - (p `3_3))) is Element of the carrier of PS
PS is non empty non degenerated non trivial right_complementable almost_left_invertible V92() associative commutative right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed doubleLoopStr
(PS) is non empty () ()
(PS) is non empty set
the carrier of PS is non empty non trivial set
[: the carrier of PS, the carrier of PS, the carrier of PS:] is non empty set
(PS) is ((PS))
(PS) is set
((PS),(PS)) is () ()
the carrier of (PS) is non empty set
a is Element of the carrier of (PS)
b is Element of the carrier of (PS)
c is Element of the carrier of (PS)
[a,b,c,c] is Element of [: the carrier of (PS), the carrier of (PS), the carrier of (PS), the carrier of (PS):]
[: the carrier of (PS), the carrier of (PS), the carrier of (PS), the carrier of (PS):] is non empty set
p is Element of [: the carrier of PS, the carrier of PS, the carrier of PS:]
q is Element of [: the carrier of PS, the carrier of PS, the carrier of PS:]
s is Element of [: the carrier of PS, the carrier of PS, the carrier of PS:]
[p,q,s,s] is Element of [:[: the carrier of PS, the carrier of PS, the carrier of PS:],[: the carrier of PS, the carrier of PS, the carrier of PS:],[: the carrier of PS, the carrier of PS, the carrier of PS:],[: the carrier of PS, the carrier of PS, the carrier of PS:]:]
[:[: the carrier of PS, the carrier of PS, the carrier of PS:],[: the carrier of PS, the carrier of PS, the carrier of PS:],[: the carrier of PS, the carrier of PS, the carrier of PS:],[: the carrier of PS, the carrier of PS, the carrier of PS:]:] is non empty set
p `2_3 is Element of the carrier of PS
q `2_3 is Element of the carrier of PS
(p `2_3) - (q `2_3) is Element of the carrier of PS
s `3_3 is Element of the carrier of PS
(s `3_3) - (s `3_3) is Element of the carrier of PS
((p `2_3) - (q `2_3)) * ((s `3_3) - (s `3_3)) is Element of the carrier of PS
s `2_3 is Element of the carrier of PS
(s `2_3) - (s `2_3) is Element of the carrier of PS
p `3_3 is Element of the carrier of PS
q `3_3 is Element of the carrier of PS
(p `3_3) - (q `3_3) is Element of the carrier of PS
((s `2_3) - (s `2_3)) * ((p `3_3) - (q `3_3)) is Element of the carrier of PS
(((p `2_3) - (q `2_3)) * ((s `3_3) - (s `3_3))) - (((s `2_3) - (s `2_3)) * ((p `3_3) - (q `3_3))) is Element of the carrier of PS
0. PS is V49(PS) Element of the carrier of PS
the ZeroF of PS is Element of the carrier of PS
p `1_3 is Element of the carrier of PS
q `1_3 is Element of the carrier of PS
(p `1_3) - (q `1_3) is Element of the carrier of PS
((p `1_3) - (q `1_3)) * ((s `2_3) - (s `2_3)) is Element of the carrier of PS
s `1_3 is Element of the carrier of PS
(s `1_3) - (s `1_3) is Element of the carrier of PS
((s `1_3) - (s `1_3)) * ((p `2_3) - (q `2_3)) is Element of the carrier of PS
(((p `1_3) - (q `1_3)) * ((s `2_3) - (s `2_3))) - (((s `1_3) - (s `1_3)) * ((p `2_3) - (q `2_3))) is Element of the carrier of PS
((p `1_3) - (q `1_3)) * ((s `3_3) - (s `3_3)) is Element of the carrier of PS
((s `1_3) - (s `1_3)) * ((p `3_3) - (q `3_3)) is Element of the carrier of PS
(((p `1_3) - (q `1_3)) * ((s `3_3) - (s `3_3))) - (((s `1_3) - (s `1_3)) * ((p `3_3) - (q `3_3))) is Element of the carrier of PS
PS is non empty non degenerated non trivial right_complementable almost_left_invertible V92() associative commutative right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed doubleLoopStr
(PS) is non empty () ()
(PS) is non empty set
the carrier of PS is non empty non trivial set
[: the carrier of PS, the carrier of PS, the carrier of PS:] is non empty set
(PS) is ((PS))
(PS) is set
((PS),(PS)) is () ()
the carrier of (PS) is non empty set
a is Element of the carrier of (PS)
b is Element of the carrier of (PS)
c is Element of the carrier of (PS)
p is Element of the carrier of (PS)
q is Element of the carrier of (PS)
s is Element of the carrier of (PS)
0. PS is V49(PS) Element of the carrier of PS
the ZeroF of PS is Element of the carrier of PS
[a,b,c,p] is Element of [: the carrier of (PS), the carrier of (PS), the carrier of (PS), the carrier of (PS):]
[: the carrier of (PS), the carrier of (PS), the carrier of (PS), the carrier of (PS):] is non empty set
s is Element of [: the carrier of PS, the carrier of PS, the carrier of PS:]
s is Element of [: the carrier of PS, the carrier of PS, the carrier of PS:]
c₁₀ is Element of [: the carrier of PS, the carrier of PS, the carrier of PS:]
h is Element of [: the carrier of PS, the carrier of PS, the carrier of PS:]
[s,s,c₁₀,h] is Element of [:[: the carrier of PS, the carrier of PS, the carrier of PS:],[: the carrier of PS, the carrier of PS, the carrier of PS:],[: the carrier of PS, the carrier of PS, the carrier of PS:],[: the carrier of PS, the carrier of PS, the carrier of PS:]:]
[:[: the carrier of PS, the carrier of PS, the carrier of PS:],[: the carrier of PS, the carrier of PS, the carrier of PS:],[: the carrier of PS, the carrier of PS, the carrier of PS:],[: the carrier of PS, the carrier of PS, the carrier of PS:]:] is non empty set
s `1_3 is Element of the carrier of PS
s `1_3 is Element of the carrier of PS
(s `1_3) - (s `1_3) is Element of the carrier of PS
c₁₀ `2_3 is Element of the carrier of PS
h `2_3 is Element of the carrier of PS
(c₁₀ `2_3) - (h `2_3) is Element of the carrier of PS
((s `1_3) - (s `1_3)) * ((c₁₀ `2_3) - (h `2_3)) is Element of the carrier of PS
c₁₀ `1_3 is Element of the carrier of PS
h `1_3 is Element of the carrier of PS
(c₁₀ `1_3) - (h `1_3) is Element of the carrier of PS
s `2_3 is Element of the carrier of PS
s `2_3 is Element of the carrier of PS
(s `2_3) - (s `2_3) is Element of the carrier of PS
((c₁₀ `1_3) - (h `1_3)) * ((s `2_3) - (s `2_3)) is Element of the carrier of PS
(((s `1_3) - (s `1_3)) * ((c₁₀ `2_3) - (h `2_3))) - (((c₁₀ `1_3) - (h `1_3)) * ((s `2_3) - (s `2_3))) is Element of the carrier of PS
c₁₀ `3_3 is Element of the carrier of PS
h `3_3 is Element of the carrier of PS
(c₁₀ `3_3) - (h `3_3) is Element of the carrier of PS
((s `1_3) - (s `1_3)) * ((c₁₀ `3_3) - (h `3_3)) is Element of the carrier of PS
s `3_3 is Element of the carrier of PS
s `3_3 is Element of the carrier of PS
(s `3_3) - (s `3_3) is Element of the carrier of PS
((c₁₀ `1_3) - (h `1_3)) * ((s `3_3) - (s `3_3)) is Element of the carrier of PS
(((s `1_3) - (s `1_3)) * ((c₁₀ `3_3) - (h `3_3))) - (((c₁₀ `1_3) - (h `1_3)) * ((s `3_3) - (s `3_3))) is Element of the carrier of PS
((s `2_3) - (s `2_3)) * ((c₁₀ `3_3) - (h `3_3)) is Element of the carrier of PS
((c₁₀ `2_3) - (h `2_3)) * ((s `3_3) - (s `3_3)) is Element of the carrier of PS
(((s `2_3) - (s `2_3)) * ((c₁₀ `3_3) - (h `3_3))) - (((c₁₀ `2_3) - (h `2_3)) * ((s `3_3) - (s `3_3))) is Element of the carrier of PS
[a,b,q,s] is Element of [: the carrier of (PS), the carrier of (PS), the carrier of (PS), the carrier of (PS):]
i is Element of [: the carrier of PS, the carrier of PS, the carrier of PS:]
j is Element of [: the carrier of PS, the carrier of PS, the carrier of PS:]
k is Element of [: the carrier of PS, the carrier of PS, the carrier of PS:]
l is Element of [: the carrier of PS, the carrier of PS, the carrier of PS:]
[i,j,k,l] is Element of [:[: the carrier of PS, the carrier of PS, the carrier of PS:],[: the carrier of PS, the carrier of PS, the carrier of PS:],[: the carrier of PS, the carrier of PS, the carrier of PS:],[: the carrier of PS, the carrier of PS, the carrier of PS:]:]
i `1_3 is Element of the carrier of PS
j `1_3 is Element of the carrier of PS
(i `1_3) - (j `1_3) is Element of the carrier of PS
k `2_3 is Element of the carrier of PS
l `2_3 is Element of the carrier of PS
(k `2_3) - (l `2_3) is Element of the carrier of PS
((i `1_3) - (j `1_3)) * ((k `2_3) - (l `2_3)) is Element of the carrier of PS
k `1_3 is Element of the carrier of PS
l `1_3 is Element of the carrier of PS
(k `1_3) - (l `1_3) is Element of the carrier of PS
i `2_3 is Element of the carrier of PS
j `2_3 is Element of the carrier of PS
(i `2_3) - (j `2_3) is Element of the carrier of PS
((k `1_3) - (l `1_3)) * ((i `2_3) - (j `2_3)) is Element of the carrier of PS
(((i `1_3) - (j `1_3)) * ((k `2_3) - (l `2_3))) - (((k `1_3) - (l `1_3)) * ((i `2_3) - (j `2_3))) is Element of the carrier of PS
k `3_3 is Element of the carrier of PS
l `3_3 is Element of the carrier of PS
(k `3_3) - (l `3_3) is Element of the carrier of PS
((i `1_3) - (j `1_3)) * ((k `3_3) - (l `3_3)) is Element of the carrier of PS
i `3_3 is Element of the carrier of PS
j `3_3 is Element of the carrier of PS
(i `3_3) - (j `3_3) is Element of the carrier of PS
((k `1_3) - (l `1_3)) * ((i `3_3) - (j `3_3)) is Element of the carrier of PS
(((i `1_3) - (j `1_3)) * ((k `3_3) - (l `3_3))) - (((k `1_3) - (l `1_3)) * ((i `3_3) - (j `3_3))) is Element of the carrier of PS
((i `2_3) - (j `2_3)) * ((k `3_3) - (l `3_3)) is Element of the carrier of PS
((k `2_3) - (l `2_3)) * ((i `3_3) - (j `3_3)) is Element of the carrier of PS
(((i `2_3) - (j `2_3)) * ((k `3_3) - (l `3_3))) - (((k `2_3) - (l `2_3)) * ((i `3_3) - (j `3_3))) is Element of the carrier of PS
[(s `1_3),(s `2_3),(s `3_3)] is Element of [: the carrier of PS, the carrier of PS, the carrier of PS:]
((c<sub>10</sub> `1_3) - (h `1_3)) * ((k `2_3) - (l `2_3)) is Element of the carrier of PS
((k `1_3) - (l `1_3)) * ((c<sub>10</sub> `2_3) - (h `2_3)) is Element of the carrier of PS
(((c<sub>10</sub> `1_3) - (h `1_3)) * ((k `2_3) - (l `2_3))) - (((k `1_3) - (l `1_3)) * ((c<sub>10</sub> `2_3) - (h `2_3))) is Element of the carrier of PS
((c<sub>10</sub> `1_3) - (h `1_3)) * ((k `3_3) - (l `3_3)) is Element of the carrier of PS
((k `1_3) - (l `1_3)) * ((c<sub>10</sub> `3_3) - (h `3_3)) is Element of the carrier of PS
(((c<sub>10</sub> `1_3) - (h `1_3)) * ((k `3_3) - (l `3_3))) - (((k `1_3) - (l `1_3)) * ((c<sub>10</sub> `3_3) - (h `3_3))) is Element of the carrier of PS
((c<sub>10</sub> `2_3) - (h `2_3)) * ((k `3_3) - (l `3_3)) is Element of the carrier of PS
((s `1_3) - (s `1_3)) " is Element of the carrier of PS
(((c<sub>10</sub> `1_3) - (h `1_3)) * ((s `2_3) - (s `2_3))) * (((s `1_3) - (s `1_3)) ") is Element of the carrier of PS
((((c<sub>10</sub> `1_3) - (h `1_3)) * ((s `2_3) - (s `2_3))) * (((s `1_3) - (s `1_3)) ")) * ((k `3_3) - (l `3_3)) is Element of the carrier of PS
((k `2_3) - (l `2_3)) * ((c<sub>10</sub> `3_3) - (h `3_3)) is Element of the carrier of PS
((k `1_3) - (l `1_3)) * ((s `2_3) - (s `2_3)) is Element of the carrier of PS
(((k `1_3) - (l `1_3)) * ((s `2_3) - (s `2_3))) * (((s `1_3) - (s `1_3)) ") is Element of the carrier of PS
((((k `1_3) - (l `1_3)) * ((s `2_3) - (s `2_3))) * (((s `1_3) - (s `1_3)) ")) * ((c<sub>10</sub> `3_3) - (h `3_3)) is Element of the carrier of PS
(((c<sub>10</sub> `2_3) - (h `2_3)) * ((k `3_3) - (l `3_3))) - (((k `2_3) - (l `2_3)) * ((c<sub>10</sub> `3_3) - (h `3_3))) is Element of the carrier of PS
((c<sub>10</sub> `1_3) - (h `1_3)) * ((k `2_3) - (l `2_3)) is Element of the carrier of PS
((k `1_3) - (l `1_3)) * ((c<sub>10</sub> `2_3) - (h `2_3)) is Element of the carrier of PS
(((c<sub>10</sub> `1_3) - (h `1_3)) * ((k `2_3) - (l `2_3))) - (((k `1_3) - (l `1_3)) * ((c<sub>10</sub> `2_3) - (h `2_3))) is Element of the carrier of PS
((c<sub>10</sub> `2_3) - (h `2_3)) * ((k `3_3) - (l `3_3)) is Element of the carrier of PS
((k `2_3) - (l `2_3)) * ((c<sub>10</sub> `3_3) - (h `3_3)) is Element of the carrier of PS
(((c<sub>10</sub> `2_3) - (h `2_3)) * ((k `3_3) - (l `3_3))) - (((k `2_3) - (l `2_3)) * ((c<sub>10</sub> `3_3) - (h `3_3))) is Element of the carrier of PS
((c<sub>10</sub> `1_3) - (h `1_3)) * ((k `3_3) - (l `3_3)) is Element of the carrier of PS
((c<sub>10</sub> `2_3) - (h `2_3)) * ((s `1_3) - (s `1_3)) is Element of the carrier of PS
((s `2_3) - (s `2_3)) " is Element of the carrier of PS
(((c<sub>10</sub> `2_3) - (h `2_3)) * ((s `1_3) - (s `1_3))) * (((s `2_3) - (s `2_3)) ") is Element of the carrier of PS
((((c<sub>10</sub> `2_3) - (h `2_3)) * ((s `1_3) - (s `1_3))) * (((s `2_3) - (s `2_3)) ")) * ((k `3_3) - (l `3_3)) is Element of the carrier of PS
((k `1_3) - (l `1_3)) * ((c<sub>10</sub> `3_3) - (h `3_3)) is Element of the carrier of PS
((k `2_3) - (l `2_3)) * ((s `1_3) - (s `1_3)) is Element of the carrier of PS
(((k `2_3) - (l `2_3)) * ((s `1_3) - (s `1_3))) * (((s `2_3) - (s `2_3)) ") is Element of the carrier of PS
((((k `2_3) - (l `2_3)) * ((s `1_3) - (s `1_3))) * (((s `2_3) - (s `2_3)) ")) * ((c<sub>10</sub> `3_3) - (h `3_3)) is Element of the carrier of PS
(((c<sub>10</sub> `1_3) - (h `1_3)) * ((k `3_3) - (l `3_3))) - (((k `1_3) - (l `1_3)) * ((c<sub>10</sub> `3_3) - (h `3_3))) is Element of the carrier of PS
((c<sub>10</sub> `2_3) - (h `2_3)) * ((k `3_3) - (l `3_3)) is Element of the carrier of PS
((k `2_3) - (l `2_3)) * ((c<sub>10</sub> `3_3) - (h `3_3)) is Element of the carrier of PS
(((c<sub>10</sub> `2_3) - (h `2_3)) * ((k `3_3) - (l `3_3))) - (((k `2_3) - (l `2_3)) * ((c<sub>10</sub> `3_3) - (h `3_3))) is Element of the carrier of PS
((c<sub>10</sub> `1_3) - (h `1_3)) * ((k `2_3) - (l `2_3)) is Element of the carrier of PS
((c<sub>10</sub> `3_3) - (h `3_3)) * ((s `1_3) - (s `1_3)) is Element of the carrier of PS
((s `3_3) - (s `3_3)) " is Element of the carrier of PS
(((c<sub>10</sub> `3_3) - (h `3_3)) * ((s `1_3) - (s `1_3))) * (((s `3_3) - (s `3_3)) ") is Element of the carrier of PS
((((c<sub>10</sub> `3_3) - (h `3_3)) * ((s `1_3) - (s `1_3))) * (((s `3_3) - (s `3_3)) ")) * ((k `2_3) - (l `2_3)) is Element of the carrier of PS
((k `1_3) - (l `1_3)) * ((c<sub>10</sub> `2_3) - (h `2_3)) is Element of the carrier of PS
((k `3_3) - (l `3_3)) * ((s `1_3) - (s `1_3)) is Element of the carrier of PS
(((k `3_3) - (l `3_3)) * ((s `1_3) - (s `1_3))) * (((s `3_3) - (s `3_3)) ") is Element of the carrier of PS
((((k `3_3) - (l `3_3)) * ((s `1_3) - (s `1_3))) * (((s `3_3) - (s `3_3)) ")) * ((c<sub>10</sub> `2_3) - (h `2_3)) is Element of the carrier of PS
((c<sub>10</sub> `3_3) - (h `3_3)) * ((k `2_3) - (l `2_3)) is Element of the carrier of PS
((k `3_3) - (l `3_3)) * ((c<sub>10</sub> `2_3) - (h `2_3)) is Element of the carrier of PS
(((c<sub>10</sub> `3_3) - (h `3_3)) * ((k `2_3) - (l `2_3))) - (((k `3_3) - (l `3_3)) * ((c<sub>10</sub> `2_3) - (h `2_3))) is Element of the carrier of PS
(((c<sub>10</sub> `1_3) - (h `1_3)) * ((k `2_3) - (l `2_3))) - (((k `1_3) - (l `1_3)) * ((c<sub>10</sub> `2_3) - (h `2_3))) is Element of the carrier of PS
((c<sub>10</sub> `1_3) - (h `1_3)) * ((k `3_3) - (l `3_3)) is Element of the carrier of PS
((k `1_3) - (l `1_3)) * ((c<sub>10</sub> `3_3) - (h `3_3)) is Element of the carrier of PS
(((c<sub>10</sub> `1_3) - (h `1_3)) * ((k `3_3) - (l `3_3))) - (((k `1_3) - (l `1_3)) * ((c<sub>10</sub> `3_3) - (h `3_3))) is Element of the carrier of PS
((c<sub>10</sub> `1_3) - (h `1_3)) * ((k `2_3) - (l `2_3)) is Element of the carrier of PS
((k `1_3) - (l `1_3)) * ((c<sub>10</sub> `2_3) - (h `2_3)) is Element of the carrier of PS
(((c<sub>10</sub> `1_3) - (h `1_3)) * ((k `2_3) - (l `2_3))) - (((k `1_3) - (l `1_3)) * ((c<sub>10</sub> `2_3) - (h `2_3))) is Element of the carrier of PS
((c<sub>10</sub> `1_3) - (h `1_3)) * ((k `3_3) - (l `3_3)) is Element of the carrier of PS
((k `1_3) - (l `1_3)) * ((c<sub>10</sub> `3_3) - (h `3_3)) is Element of the carrier of PS
(((c<sub>10</sub> `1_3) - (h `1_3)) * ((k `3_3) - (l `3_3))) - (((k `1_3) - (l `1_3)) * ((c<sub>10</sub> `3_3) - (h `3_3))) is Element of the carrier of PS
((c<sub>10</sub> `2_3) - (h `2_3)) * ((k `3_3) - (l `3_3)) is Element of the carrier of PS
((k `2_3) - (l `2_3)) * ((c<sub>10</sub> `3_3) - (h `3_3)) is Element of the carrier of PS
(((c<sub>10</sub> `2_3) - (h `2_3)) * ((k `3_3) - (l `3_3))) - (((k `2_3) - (l `2_3)) * ((c<sub>10</sub> `3_3) - (h `3_3))) is Element of the carrier of PS
((c<sub>10</sub> `1_3) - (h `1_3)) * ((k `2_3) - (l `2_3)) is Element of the carrier of PS
((k `1_3) - (l `1_3)) * ((c<sub>10</sub> `2_3) - (h `2_3)) is Element of the carrier of PS
(((c<sub>10</sub> `1_3) - (h `1_3)) * ((k `2_3) - (l `2_3))) - (((k `1_3) - (l `1_3)) * ((c<sub>10</sub> `2_3) - (h `2_3))) is Element of the carrier of PS
((c<sub>10</sub> `1_3) - (h `1_3)) * ((k `3_3) - (l `3_3)) is Element of the carrier of PS
((k `1_3) - (l `1_3)) * ((c<sub>10</sub> `3_3) - (h `3_3)) is Element of the carrier of PS
(((c<sub>10</sub> `1_3) - (h `1_3)) * ((k `3_3) - (l `3_3))) - (((k `1_3) - (l `1_3)) * ((c<sub>10</sub> `3_3) - (h `3_3))) is Element of the carrier of PS
((c<sub>10</sub> `2_3) - (h `2_3)) * ((k `3_3) - (l `3_3)) is Element of the carrier of PS
((k `2_3) - (l `2_3)) * ((c<sub>10</sub> `3_3) - (h `3_3)) is Element of the carrier of PS
(((c<sub>10</sub> `2_3) - (h `2_3)) * ((k `3_3) - (l `3_3))) - (((k `2_3) - (l `2_3)) * ((c<sub>10</sub> `3_3) - (h `3_3))) is Element of the carrier of PS
[c,p,q,s] is Element of [: the carrier of (PS), the carrier of (PS), the carrier of (PS), the carrier of (PS):]
c<sub>25</sub> is Element of [: the carrier of PS, the carrier of PS, the carrier of PS:]
c<sub>26</sub> is Element of [: the carrier of PS, the carrier of PS, the carrier of PS:]
c<sub>27</sub> is Element of [: the carrier of PS, the carrier of PS, the carrier of PS:]
c<sub>28</sub> is Element of [: the carrier of PS, the carrier of PS, the carrier of PS:]
[c<sub>25</sub>,c<sub>26</sub>,c<sub>27</sub>,c<sub>28</sub>] is Element of [:[: the carrier of PS, the carrier of PS, the carrier of PS:],[: the carrier of PS, the carrier of PS, the carrier of PS:],[: the carrier of PS, the carrier of PS, the carrier of PS:],[: the carrier of PS, the carrier of PS, the carrier of PS:]:]
c<sub>25</sub> `1_3 is Element of the carrier of PS
c₂₆ `1_3 is Element of the carrier of PS
(c<sub>25</sub> `1_3) - (c₂₆ `1_3) is Element of the carrier of PS
c<sub>27</sub> `2_3 is Element of the carrier of PS
c₂₈ `2_3 is Element of the carrier of PS
(c<sub>27</sub> `2_3) - (c₂₈ `2_3) is Element of the carrier of PS
((c<sub>25</sub> `1_3) - (c₂₆ `1_3)) * ((c<sub>27</sub> `2_3) - (c₂₈ `2_3)) is Element of the carrier of PS
c<sub>27</sub> `1_3 is Element of the carrier of PS
c₂₈ `1_3 is Element of the carrier of PS
(c<sub>27</sub> `1_3) - (c₂₈ `1_3) is Element of the carrier of PS
c<sub>25</sub> `2_3 is Element of the carrier of PS
c₂₆ `2_3 is Element of the carrier of PS
(c<sub>25</sub> `2_3) - (c₂₆ `2_3) is Element of the carrier of PS
((c<sub>27</sub> `1_3) - (c₂₈ `1_3)) * ((c<sub>25</sub> `2_3) - (c₂₆ `2_3)) is Element of the carrier of PS
(((c<sub>25</sub> `1_3) - (c₂₆ `1_3)) * ((c<sub>27</sub> `2_3) - (c₂₈ `2_3))) - (((c<sub>27</sub> `1_3) - (c₂₈ `1_3)) * ((c<sub>25</sub> `2_3) - (c₂₆ `2_3))) is Element of the carrier of PS
c<sub>27</sub> `3_3 is Element of the carrier of PS
c₂₈ `3_3 is Element of the carrier of PS
(c<sub>27</sub> `3_3) - (c₂₈ `3_3) is Element of the carrier of PS
((c<sub>25</sub> `1_3) - (c₂₆ `1_3)) * ((c<sub>27</sub> `3_3) - (c₂₈ `3_3)) is Element of the carrier of PS
c<sub>25</sub> `3_3 is Element of the carrier of PS
c₂₆ `3_3 is Element of the carrier of PS
(c<sub>25</sub> `3_3) - (c₂₆ `3_3) is Element of the carrier of PS
((c<sub>27</sub> `1_3) - (c₂₈ `1_3)) * ((c<sub>25</sub> `3_3) - (c₂₆ `3_3)) is Element of the carrier of PS
(((c<sub>25</sub> `1_3) - (c₂₆ `1_3)) * ((c<sub>27</sub> `3_3) - (c₂₈ `3_3))) - (((c<sub>27</sub> `1_3) - (c₂₈ `1_3)) * ((c<sub>25</sub> `3_3) - (c₂₆ `3_3))) is Element of the carrier of PS
((c<sub>25</sub> `2_3) - (c₂₆ `2_3)) * ((c<sub>27</sub> `3_3) - (c₂₈ `3_3)) is Element of the carrier of PS
((c<sub>27</sub> `2_3) - (c₂₈ `2_3)) * ((c<sub>25</sub> `3_3) - (c₂₆ `3_3)) is Element of the carrier of PS
(((c<sub>25</sub> `2_3) - (c₂₆ `2_3)) * ((c<sub>27</sub> `3_3) - (c₂₈ `3_3))) - (((c<sub>27</sub> `2_3) - (c₂₈ `2_3)) * ((c<sub>25</sub> `3_3) - (c₂₆ `3_3))) is Element of the carrier of PS
PS is non empty non degenerated non trivial right_complementable almost_left_invertible V92() associative commutative right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed doubleLoopStr
(PS) is non empty () ()
(PS) is non empty set
the carrier of PS is non empty non trivial set
[: the carrier of PS, the carrier of PS, the carrier of PS:] is non empty set
(PS) is ((PS))
(PS) is set
((PS),(PS)) is () ()
the carrier of (PS) is non empty set
a is Element of the carrier of (PS)
b is Element of the carrier of (PS)
c is Element of the carrier of (PS)
[a,b,a,c] is Element of [: the carrier of (PS), the carrier of (PS), the carrier of (PS), the carrier of (PS):]
[: the carrier of (PS), the carrier of (PS), the carrier of (PS), the carrier of (PS):] is non empty set
0. PS is V49(PS) Element of the carrier of PS
the ZeroF of PS is Element of the carrier of PS
p is Element of [: the carrier of PS, the carrier of PS, the carrier of PS:]
q is Element of [: the carrier of PS, the carrier of PS, the carrier of PS:]
s is Element of [: the carrier of PS, the carrier of PS, the carrier of PS:]
s is Element of [: the carrier of PS, the carrier of PS, the carrier of PS:]
[p,q,s,s] is Element of [:[: the carrier of PS, the carrier of PS, the carrier of PS:],[: the carrier of PS, the carrier of PS, the carrier of PS:],[: the carrier of PS, the carrier of PS, the carrier of PS:],[: the carrier of PS, the carrier of PS, the carrier of PS:]:]
[:[: the carrier of PS, the carrier of PS, the carrier of PS:],[: the carrier of PS, the carrier of PS, the carrier of PS:],[: the carrier of PS, the carrier of PS, the carrier of PS:],[: the carrier of PS, the carrier of PS, the carrier of PS:]:] is non empty set
p `1_3 is Element of the carrier of PS
q `1_3 is Element of the carrier of PS
(p `1_3) - (q `1_3) is Element of the carrier of PS
s `2_3 is Element of the carrier of PS
s `2_3 is Element of the carrier of PS
(s `2_3) - (s `2_3) is Element of the carrier of PS
((p `1_3) - (q `1_3)) * ((s `2_3) - (s `2_3)) is Element of the carrier of PS
s `1_3 is Element of the carrier of PS
s `1_3 is Element of the carrier of PS
(s `1_3) - (s `1_3) is Element of the carrier of PS
p `2_3 is Element of the carrier of PS
q `2_3 is Element of the carrier of PS
(p `2_3) - (q `2_3) is Element of the carrier of PS
((s `1_3) - (s `1_3)) * ((p `2_3) - (q `2_3)) is Element of the carrier of PS
(((p `1_3) - (q `1_3)) * ((s `2_3) - (s `2_3))) - (((s `1_3) - (s `1_3)) * ((p `2_3) - (q `2_3))) is Element of the carrier of PS
s `3_3 is Element of the carrier of PS
s `3_3 is Element of the carrier of PS
(s `3_3) - (s `3_3) is Element of the carrier of PS
((p `1_3) - (q `1_3)) * ((s `3_3) - (s `3_3)) is Element of the carrier of PS
p `3_3 is Element of the carrier of PS
q `3_3 is Element of the carrier of PS
(p `3_3) - (q `3_3) is Element of the carrier of PS
((s `1_3) - (s `1_3)) * ((p `3_3) - (q `3_3)) is Element of the carrier of PS
(((p `1_3) - (q `1_3)) * ((s `3_3) - (s `3_3))) - (((s `1_3) - (s `1_3)) * ((p `3_3) - (q `3_3))) is Element of the carrier of PS
((p `2_3) - (q `2_3)) * ((s `3_3) - (s `3_3)) is Element of the carrier of PS
((s `2_3) - (s `2_3)) * ((p `3_3) - (q `3_3)) is Element of the carrier of PS
(((p `2_3) - (q `2_3)) * ((s `3_3) - (s `3_3))) - (((s `2_3) - (s `2_3)) * ((p `3_3) - (q `3_3))) is Element of the carrier of PS
(q `2_3) - (p `2_3) is Element of the carrier of PS
(q `3_3) - (s `3_3) is Element of the carrier of PS
((q `2_3) - (p `2_3)) * ((q `3_3) - (s `3_3)) is Element of the carrier of PS
(q `2_3) - (s `2_3) is Element of the carrier of PS
(q `3_3) - (p `3_3) is Element of the carrier of PS
((q `2_3) - (s `2_3)) * ((q `3_3) - (p `3_3)) is Element of the carrier of PS
(((q `2_3) - (p `2_3)) * ((q `3_3) - (s `3_3))) - (((q `2_3) - (s `2_3)) * ((q `3_3) - (p `3_3))) is Element of the carrier of PS
[q,p,q,s] is Element of [:[: the carrier of PS, the carrier of PS, the carrier of PS:],[: the carrier of PS, the carrier of PS, the carrier of PS:],[: the carrier of PS, the carrier of PS, the carrier of PS:],[: the carrier of PS, the carrier of PS, the carrier of PS:]:]
[b,a,b,c] is Element of [: the carrier of (PS), the carrier of (PS), the carrier of (PS), the carrier of (PS):]
(q `1_3) - (p `1_3) is Element of the carrier of PS
((q `1_3) - (p `1_3)) * ((q `2_3) - (s `2_3)) is Element of the carrier of PS
(q `1_3) - (s `1_3) is Element of the carrier of PS
((q `1_3) - (s `1_3)) * ((q `2_3) - (p `2_3)) is Element of the carrier of PS
(((q `1_3) - (p `1_3)) * ((q `2_3) - (s `2_3))) - (((q `1_3) - (s `1_3)) * ((q `2_3) - (p `2_3))) is Element of the carrier of PS
((q `1_3) - (p `1_3)) * ((q `3_3) - (s `3_3)) is Element of the carrier of PS
((q `1_3) - (s `1_3)) * ((q `3_3) - (p `3_3)) is Element of the carrier of PS
(((q `1_3) - (p `1_3)) * ((q `3_3) - (s `3_3))) - (((q `1_3) - (s `1_3)) * ((q `3_3) - (p `3_3))) is Element of the carrier of PS
PS is non empty non degenerated non trivial right_complementable almost_left_invertible V92() associative commutative right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed doubleLoopStr
(PS) is non empty () ()
(PS) is non empty set
the carrier of PS is non empty non trivial set
[: the carrier of PS, the carrier of PS, the carrier of PS:] is non empty set
(PS) is ((PS))
(PS) is set
((PS),(PS)) is () ()
the carrier of (PS) is non empty set
a is Element of the carrier of (PS)
b is Element of the carrier of (PS)
c is Element of the carrier of (PS)
p is Element of [: the carrier of PS, the carrier of PS, the carrier of PS:]
q is Element of [: the carrier of PS, the carrier of PS, the carrier of PS:]
s is Element of [: the carrier of PS, the carrier of PS, the carrier of PS:]
(PS,s,q) is Element of [: the carrier of PS, the carrier of PS, the carrier of PS:]
(PS) is V6() V18([:[: the carrier of PS, the carrier of PS, the carrier of PS:],[: the carrier of PS, the carrier of PS, the carrier of PS:]:],[: the carrier of PS, the carrier of PS, the carrier of PS:]) Element of bool [:[:[: the carrier of PS, the carrier of PS, the carrier of PS:],[: the carrier of PS, the carrier of PS, the carrier of PS:]:],[: the carrier of PS, the carrier of PS, the carrier of PS:]:]
[:[: the carrier of PS, the carrier of PS, the carrier of PS:],[: the carrier of PS, the carrier of PS, the carrier of PS:]:] is non empty set
[:[:[: the carrier of PS, the carrier of PS, the carrier of PS:],[: the carrier of PS, the carrier of PS, the carrier of PS:]:],[: the carrier of PS, the carrier of PS, the carrier of PS:]:] is non empty set
bool [:[:[: the carrier of PS, the carrier of PS, the carrier of PS:],[: the carrier of PS, the carrier of PS, the carrier of PS:]:],[: the carrier of PS, the carrier of PS, the carrier of PS:]:] is non empty set
(PS) . (s,q) is Element of [: the carrier of PS, the carrier of PS, the carrier of PS:]
(PS,p) is Element of [: the carrier of PS, the carrier of PS, the carrier of PS:]
(PS) is V6() V18([: the carrier of PS, the carrier of PS, the carrier of PS:],[: the carrier of PS, the carrier of PS, the carrier of PS:]) Element of bool [:[: the carrier of PS, the carrier of PS, the carrier of PS:],[: the carrier of PS, the carrier of PS, the carrier of PS:]:]
bool [:[: the carrier of PS, the carrier of PS, the carrier of PS:],[: the carrier of PS, the carrier of PS, the carrier of PS:]:] is non empty set
(PS) . p is Element of [: the carrier of PS, the carrier of PS, the carrier of PS:]
(PS,(PS,s,q),(PS,p)) is Element of [: the carrier of PS, the carrier of PS, the carrier of PS:]
(PS) . ((PS,s,q),(PS,p)) is Element of [: the carrier of PS, the carrier of PS, the carrier of PS:]
[p,q,s,(PS,(PS,s,q),(PS,p))] is Element of [:[: the carrier of PS, the carrier of PS, the carrier of PS:],[: the carrier of PS, the carrier of PS, the carrier of PS:],[: the carrier of PS, the carrier of PS, the carrier of PS:],[: the carrier of PS, the carrier of PS, the carrier of PS:]:]
[:[: the carrier of PS, the carrier of PS, the carrier of PS:],[: the carrier of PS, the carrier of PS, the carrier of PS:],[: the carrier of PS, the carrier of PS, the carrier of PS:],[: the carrier of PS, the carrier of PS, the carrier of PS:]:] is non empty set
s is Element of the carrier of (PS)
[a,b,c,s] is Element of [: the carrier of (PS), the carrier of (PS), the carrier of (PS), the carrier of (PS):]
[: the carrier of (PS), the carrier of (PS), the carrier of (PS), the carrier of (PS):] is non empty set
s `1_3 is Element of the carrier of PS
q `1_3 is Element of the carrier of PS
(s `1_3) + (q `1_3) is Element of the carrier of PS
s `2_3 is Element of the carrier of PS
q `2_3 is Element of the carrier of PS
(s `2_3) + (q `2_3) is Element of the carrier of PS
s `3_3 is Element of the carrier of PS
q `3_3 is Element of the carrier of PS
(s `3_3) + (q `3_3) is Element of the carrier of PS
[((s `1_3) + (q `1_3)),((s `2_3) + (q `2_3)),((s `3_3) + (q `3_3))] is Element of [: the carrier of PS, the carrier of PS, the carrier of PS:]
p `1_3 is Element of the carrier of PS
- (p `1_3) is Element of the carrier of PS
p `2_3 is Element of the carrier of PS
- (p `2_3) is Element of the carrier of PS
p `3_3 is Element of the carrier of PS
- (p `3_3) is Element of the carrier of PS
[(- (p `1_3)),(- (p `2_3)),(- (p `3_3))] is Element of [: the carrier of PS, the carrier of PS, the carrier of PS:]
((s `1_3) + (q `1_3)) + (- (p `1_3)) is Element of the carrier of PS
((s `2_3) + (q `2_3)) + (- (p `2_3)) is Element of the carrier of PS
((s `3_3) + (q `3_3)) + (- (p `3_3)) is Element of the carrier of PS
[(((s `1_3) + (q `1_3)) + (- (p `1_3))),(((s `2_3) + (q `2_3)) + (- (p `2_3))),(((s `3_3) + (q `3_3)) + (- (p `3_3)))] is Element of [: the carrier of PS, the carrier of PS, the carrier of PS:]
(PS,(PS,s,q),(PS,p)) `1_3 is Element of the carrier of PS
(PS,(PS,s,q),(PS,p)) `3_3 is Element of the carrier of PS
(p `1_3) - (q `1_3) is Element of the carrier of PS
(s `3_3) - ((PS,(PS,s,q),(PS,p)) `3_3) is Element of the carrier of PS
((p `1_3) - (q `1_3)) * ((s `3_3) - ((PS,(PS,s,q),(PS,p)) `3_3)) is Element of the carrier of PS
(s `1_3) - ((PS,(PS,s,q),(PS,p)) `1_3) is Element of the carrier of PS
(p `3_3) - (q `3_3) is Element of the carrier of PS
((s `1_3) - ((PS,(PS,s,q),(PS,p)) `1_3)) * ((p `3_3) - (q `3_3)) is Element of the carrier of PS
(((p `1_3) - (q `1_3)) * ((s `3_3) - ((PS,(PS,s,q),(PS,p)) `3_3))) - (((s `1_3) - ((PS,(PS,s,q),(PS,p)) `1_3)) * ((p `3_3) - (q `3_3))) is Element of the carrier of PS
0. PS is V49(PS) Element of the carrier of PS
the ZeroF of PS is Element of the carrier of PS
(p `1_3) - (s `1_3) is Element of the carrier of PS
(q `3_3) - ((PS,(PS,s,q),(PS,p)) `3_3) is Element of the carrier of PS
((p `1_3) - (s `1_3)) * ((q `3_3) - ((PS,(PS,s,q),(PS,p)) `3_3)) is Element of the carrier of PS
(q `1_3) - ((PS,(PS,s,q),(PS,p)) `1_3) is Element of the carrier of PS
(p `3_3) - (s `3_3) is Element of the carrier of PS
((q `1_3) - ((PS,(PS,s,q),(PS,p)) `1_3)) * ((p `3_3) - (s `3_3)) is Element of the carrier of PS
(((p `1_3) - (s `1_3)) * ((q `3_3) - ((PS,(PS,s,q),(PS,p)) `3_3))) - (((q `1_3) - ((PS,(PS,s,q),(PS,p)) `1_3)) * ((p `3_3) - (s `3_3))) is Element of the carrier of PS
(PS,(PS,s,q),(PS,p)) `2_3 is Element of the carrier of PS
(p `2_3) - (q `2_3) is Element of the carrier of PS
((p `2_3) - (q `2_3)) * ((s `3_3) - ((PS,(PS,s,q),(PS,p)) `3_3)) is Element of the carrier of PS
(s `2_3) - ((PS,(PS,s,q),(PS,p)) `2_3) is Element of the carrier of PS
((s `2_3) - ((PS,(PS,s,q),(PS,p)) `2_3)) * ((p `3_3) - (q `3_3)) is Element of the carrier of PS
(((p `2_3) - (q `2_3)) * ((s `3_3) - ((PS,(PS,s,q),(PS,p)) `3_3))) - (((s `2_3) - ((PS,(PS,s,q),(PS,p)) `2_3)) * ((p `3_3) - (q `3_3))) is Element of the carrier of PS
((p `1_3) - (q `1_3)) * ((s `2_3) - ((PS,(PS,s,q),(PS,p)) `2_3)) is Element of the carrier of PS
((s `1_3) - ((PS,(PS,s,q),(PS,p)) `1_3)) * ((p `2_3) - (q `2_3)) is Element of the carrier of PS
(((p `1_3) - (q `1_3)) * ((s `2_3) - ((PS,(PS,s,q),(PS,p)) `2_3))) - (((s `1_3) - ((PS,(PS,s,q),(PS,p)) `1_3)) * ((p `2_3) - (q `2_3))) is Element of the carrier of PS
[p,s,q,(PS,(PS,s,q),(PS,p))] is Element of [:[: the carrier of PS, the carrier of PS, the carrier of PS:],[: the carrier of PS, the carrier of PS, the carrier of PS:],[: the carrier of PS, the carrier of PS, the carrier of PS:],[: the carrier of PS, the carrier of PS, the carrier of PS:]:]
[a,c,b,s] is Element of [: the carrier of (PS), the carrier of (PS), the carrier of (PS), the carrier of (PS):]
(p `2_3) - (s `2_3) is Element of the carrier of PS
((p `2_3) - (s `2_3)) * ((q `3_3) - ((PS,(PS,s,q),(PS,p)) `3_3)) is Element of the carrier of PS
(q `2_3) - ((PS,(PS,s,q),(PS,p)) `2_3) is Element of the carrier of PS
((q `2_3) - ((PS,(PS,s,q),(PS,p)) `2_3)) * ((p `3_3) - (s `3_3)) is Element of the carrier of PS
(((p `2_3) - (s `2_3)) * ((q `3_3) - ((PS,(PS,s,q),(PS,p)) `3_3))) - (((q `2_3) - ((PS,(PS,s,q),(PS,p)) `2_3)) * ((p `3_3) - (s `3_3))) is Element of the carrier of PS
((p `1_3) - (s `1_3)) * ((q `2_3) - ((PS,(PS,s,q),(PS,p)) `2_3)) is Element of the carrier of PS
((q `1_3) - ((PS,(PS,s,q),(PS,p)) `1_3)) * ((p `2_3) - (s `2_3)) is Element of the carrier of PS
(((p `1_3) - (s `1_3)) * ((q `2_3) - ((PS,(PS,s,q),(PS,p)) `2_3))) - (((q `1_3) - ((PS,(PS,s,q),(PS,p)) `1_3)) * ((p `2_3) - (s `2_3))) is Element of the carrier of PS
the non empty non degenerated non trivial right_complementable almost_left_invertible V92() associative commutative right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed doubleLoopStr is non empty non degenerated non trivial right_complementable almost_left_invertible V92() associative commutative right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed doubleLoopStr
( the non empty non degenerated non trivial right_complementable almost_left_invertible V92() associative commutative right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed doubleLoopStr ) is non empty () ()
( the non empty non degenerated non trivial right_complementable almost_left_invertible V92() associative commutative right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed doubleLoopStr ) is non empty set
the carrier of the non empty non degenerated non trivial right_complementable almost_left_invertible V92() associative commutative right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed doubleLoopStr is non empty non trivial set
[: the carrier of the non empty non degenerated non trivial right_complementable almost_left_invertible V92() associative commutative right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed doubleLoopStr , the carrier of the non empty non degenerated non trivial right_complementable almost_left_invertible V92() associative commutative right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed doubleLoopStr , the carrier of the non empty non degenerated non trivial right_complementable almost_left_invertible V92() associative commutative right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed doubleLoopStr :] is non empty set
( the non empty non degenerated non trivial right_complementable almost_left_invertible V92() associative commutative right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed doubleLoopStr ) is (( the non empty non degenerated non trivial right_complementable almost_left_invertible V92() associative commutative right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed doubleLoopStr ))
( the non empty non degenerated non trivial right_complementable almost_left_invertible V92() associative commutative right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed doubleLoopStr ) is set
(( the non empty non degenerated non trivial right_complementable almost_left_invertible V92() associative commutative right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed doubleLoopStr ),( the non empty non degenerated non trivial right_complementable almost_left_invertible V92() associative commutative right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed doubleLoopStr )) is () ()
the carrier of ( the non empty non degenerated non trivial right_complementable almost_left_invertible V92() associative commutative right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed doubleLoopStr ) is non empty set
a is Element of the carrier of ( the non empty non degenerated non trivial right_complementable almost_left_invertible V92() associative commutative right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed doubleLoopStr )
b is Element of the carrier of ( the non empty non degenerated non trivial right_complementable almost_left_invertible V92() associative commutative right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed doubleLoopStr )
c is Element of the carrier of ( the non empty non degenerated non trivial right_complementable almost_left_invertible V92() associative commutative right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed doubleLoopStr )
p is Element of the carrier of ( the non empty non degenerated non trivial right_complementable almost_left_invertible V92() associative commutative right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed doubleLoopStr )
q is Element of the carrier of ( the non empty non degenerated non trivial right_complementable almost_left_invertible V92() associative commutative right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed doubleLoopStr )
s is Element of the carrier of ( the non empty non degenerated non trivial right_complementable almost_left_invertible V92() associative commutative right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed doubleLoopStr )
s is Element of the carrier of ( the non empty non degenerated non trivial right_complementable almost_left_invertible V92() associative commutative right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed doubleLoopStr )
s is Element of the carrier of ( the non empty non degenerated non trivial right_complementable almost_left_invertible V92() associative commutative right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed doubleLoopStr )
c₁₀ is Element of the carrier of ( the non empty non degenerated non trivial right_complementable almost_left_invertible V92() associative commutative right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed doubleLoopStr )
h is Element of the carrier of ( the non empty non degenerated non trivial right_complementable almost_left_invertible V92() associative commutative right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed doubleLoopStr )
i is Element of the carrier of ( the non empty non degenerated non trivial right_complementable almost_left_invertible V92() associative commutative right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed doubleLoopStr )
j is Element of the carrier of ( the non empty non degenerated non trivial right_complementable almost_left_invertible V92() associative commutative right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed doubleLoopStr )
k is Element of the carrier of ( the non empty non degenerated non trivial right_complementable almost_left_invertible V92() associative commutative right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed doubleLoopStr )
l is Element of the carrier of ( the non empty non degenerated non trivial right_complementable almost_left_invertible V92() associative commutative right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed doubleLoopStr )
A is Element of the carrier of ( the non empty non degenerated non trivial right_complementable almost_left_invertible V92() associative commutative right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed doubleLoopStr )
B is Element of the carrier of ( the non empty non degenerated non trivial right_complementable almost_left_invertible V92() associative commutative right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed doubleLoopStr )
C is Element of the carrier of ( the non empty non degenerated non trivial right_complementable almost_left_invertible V92() associative commutative right-distributive left-distributive right_unital well-unital V102() left_unital Abelian add-associative right_zeroed doubleLoopStr )
PS is non empty () ()
the carrier of PS is non empty set
a is Element of the carrier of PS
b is Element of the carrier of PS
PS is non empty () ()
the carrier of PS is non empty set
a is Element of the carrier of PS
b is Element of the carrier of PS
c is Element of the carrier of PS
p is Element of the carrier of PS
PS is non empty () ()
the carrier of PS is non empty set
a is Element of the carrier of PS
b is Element of the carrier of PS
c is Element of the carrier of PS
PS is non empty () ()
the carrier of PS is non empty set
a is Element of the carrier of PS
b is Element of the carrier of PS
c is Element of the carrier of PS
p is Element of the carrier of PS
PS is non empty () ()
the carrier of PS is non empty set
a is Element of the carrier of PS
b is Element of the carrier of PS
c is Element of the carrier of PS
p is Element of the carrier of PS
PS is non empty () ()
the carrier of PS is non empty set
a is Element of the carrier of PS
b is Element of the carrier of PS
c is Element of the carrier of PS
p is Element of the carrier of PS
PS is non empty () ()
the carrier of PS is non empty set
a is Element of the carrier of PS
b is Element of the carrier of PS
c is Element of the carrier of PS
PS is non empty () ()
the carrier of PS is non empty set
a is Element of the carrier of PS
b is Element of the carrier of PS
c is Element of the carrier of PS
p is Element of the carrier of PS
PS is non empty () ()
the carrier of PS is non empty set
a is Element of the carrier of PS
b is Element of the carrier of PS
c is Element of the carrier of PS
p is Element of the carrier of PS
q is Element of the carrier of PS
s is Element of the carrier of PS
PS is non empty () ()
the carrier of PS is non empty set
a is Element of the carrier of PS
b is Element of the carrier of PS
c is Element of the carrier of PS
PS is non empty () ()
the carrier of PS is non empty set
a is Element of the carrier of PS
b is Element of the carrier of PS
c is Element of the carrier of PS
p is Element of the carrier of PS
PS is non empty () ()
the carrier of PS is non empty set
a is Element of the carrier of PS
b is Element of the carrier of PS
c is Element of the carrier of PS
PS is non empty () ()
the carrier of PS is non empty set
a is Element of the carrier of PS
b is Element of the carrier of PS
c is Element of the carrier of PS
p is Element of the carrier of PS
q is Element of the carrier of PS
s is Element of the carrier of PS
s is Element of the carrier of PS
s is Element of the carrier of PS
PS is non empty () ()
the carrier of PS is non empty set
a is Element of the carrier of PS
b is Element of the carrier of PS
c is Element of the carrier of PS
p is Element of the carrier of PS
q is Element of the carrier of PS
s is Element of the carrier of PS
PS is non empty () ()
the carrier of PS is non empty set
a is Element of the carrier of PS
b is Element of the carrier of PS
c is Element of the carrier of PS
p is Element of the carrier of PS
q is Element of the carrier of PS
PS is non empty () ()
the carrier of PS is non empty set
a is Element of the carrier of PS
b is Element of the carrier of PS
c is Element of the carrier of PS
p is Element of the carrier of PS
PS is non empty () ()
the carrier of PS is non empty set
a is Element of the carrier of PS
b is Element of the carrier of PS
c is Element of the carrier of PS
p is Element of the carrier of PS
q is Element of the carrier of PS
s is Element of the carrier of PS
s is Element of the carrier of PS
PS is non empty () ()
the carrier of PS is non empty set
a is Element of the carrier of PS
b is Element of the carrier of PS
c is Element of the carrier of PS
p is Element of the carrier of PS
PS is non empty () ()
the carrier of PS is non empty set
a is Element of the carrier of PS
b is Element of the carrier of PS
c is Element of the carrier of PS
p is Element of the carrier of PS
PS is non empty () ()
the carrier of PS is non empty set
a is Element of the carrier of PS
b is Element of the carrier of PS
a is Element of the carrier of PS
b is Element of the carrier of PS
c is Element of the carrier of PS
p is Element of the carrier of PS
q is Element of the carrier of PS
s is Element of the carrier of PS
PS is non empty () ()
the carrier of PS is non empty set
a is Element of the carrier of PS
b is Element of the carrier of PS
c is Element of the carrier of PS
p is Element of the carrier of PS
q is Element of the carrier of PS