:: RINGCAT1 semantic presentation

K132() is Element of bool K128()

K128() is set

bool K128() is set

K47() is set

bool K47() is set

bool K132() is set

{} is empty set

1 is non empty set

{{},1} is non empty set

K133() is empty Element of K132()

2 is non empty set

K319(K133(),1,2) is set

[:K319(K133(),1,2),K319(K133(),1,2):] is set

[:[:K319(K133(),1,2),K319(K133(),1,2):],K319(K133(),1,2):] is set

bool [:[:K319(K133(),1,2),K319(K133(),1,2):],K319(K133(),1,2):] is set

bool [:K319(K133(),1,2),K319(K133(),1,2):] is set

Z_3 is non empty right_complementable almost_left_invertible strict V96() V97() V98() unital associative commutative right-distributive left-distributive right_unital well-unital V148() left_unital Fanoian doubleLoopStr

the carrier of Z_3 is non empty set

the addF of Z_3 is V1() V4([: the carrier of Z_3, the carrier of Z_3:]) V5( the carrier of Z_3) V6() total V28([: the carrier of Z_3, the carrier of Z_3:], the carrier of Z_3) Element of bool [:[: the carrier of Z_3, the carrier of Z_3:], the carrier of Z_3:]

[: the carrier of Z_3, the carrier of Z_3:] is set

[:[: the carrier of Z_3, the carrier of Z_3:], the carrier of Z_3:] is set

bool [:[: the carrier of Z_3, the carrier of Z_3:], the carrier of Z_3:] is set

comp Z_3 is V1() V4( the carrier of Z_3) V5( the carrier of Z_3) V6() non empty total V28( the carrier of Z_3, the carrier of Z_3) Element of bool [: the carrier of Z_3, the carrier of Z_3:]

bool [: the carrier of Z_3, the carrier of Z_3:] is set

0. Z_3 is V48( Z_3 ) Element of the carrier of Z_3

the ZeroF of Z_3 is Element of the carrier of Z_3

the multF of Z_3 is V1() V4([: the carrier of Z_3, the carrier of Z_3:]) V5( the carrier of Z_3) V6() total V28([: the carrier of Z_3, the carrier of Z_3:], the carrier of Z_3) Element of bool [:[: the carrier of Z_3, the carrier of Z_3:], the carrier of Z_3:]

1. Z_3 is Element of the carrier of Z_3

the OneF of Z_3 is Element of the carrier of Z_3

UN is non empty doubleLoopStr

the carrier of UN is non empty set

a is non empty doubleLoopStr

the carrier of a is non empty set

[: the carrier of UN, the carrier of a:] is set

bool [: the carrier of UN, the carrier of a:] is set

UN is non empty doubleLoopStr

the carrier of UN is non empty set

a is non empty doubleLoopStr

the carrier of a is non empty set

[: the carrier of UN, the carrier of a:] is set

bool [: the carrier of UN, the carrier of a:] is set

aa is V1() V4( the carrier of UN) V5( the carrier of a) V6() non empty total V28( the carrier of UN, the carrier of a) Element of bool [: the carrier of UN, the carrier of a:]

aa is V1() V4( the carrier of UN) V5( the carrier of a) V6() non empty total V28( the carrier of UN, the carrier of a) Element of bool [: the carrier of UN, the carrier of a:]

UN is non empty doubleLoopStr

the carrier of UN is non empty set

a is non empty doubleLoopStr

the carrier of a is non empty set

[: the carrier of UN, the carrier of a:] is set

bool [: the carrier of UN, the carrier of a:] is set

aa is non empty doubleLoopStr

the carrier of aa is non empty set

[: the carrier of a, the carrier of aa:] is set

bool [: the carrier of a, the carrier of aa:] is set

C is V1() V4( the carrier of UN) V5( the carrier of a) V6() non empty total V28( the carrier of UN, the carrier of a) Element of bool [: the carrier of UN, the carrier of a:]

ii is V1() V4( the carrier of a) V5( the carrier of aa) V6() non empty total V28( the carrier of a, the carrier of aa) Element of bool [: the carrier of a, the carrier of aa:]

ii * C is V1() V4( the carrier of UN) V5( the carrier of aa) V6() non empty total V28( the carrier of UN, the carrier of aa) Element of bool [: the carrier of UN, the carrier of aa:]

[: the carrier of UN, the carrier of aa:] is set

bool [: the carrier of UN, the carrier of aa:] is set

ii is Element of the carrier of UN

c

ii + c

(ii * C) . (ii + c

(ii * C) . ii is Element of the carrier of aa

(ii * C) . c

((ii * C) . ii) + ((ii * C) . c

C . ii is Element of the carrier of a

ii . (C . ii) is Element of the carrier of aa

C . c

ii . (C . c

C . (ii + c

ii . (C . (ii + c

(C . ii) + (C . c

ii . ((C . ii) + (C . c

ii is Element of the carrier of UN

c

ii * c

(ii * C) . (ii * c

(ii * C) . ii is Element of the carrier of aa

(ii * C) . c

((ii * C) . ii) * ((ii * C) . c

C . ii is Element of the carrier of a

ii . (C . ii) is Element of the carrier of aa

C . c

ii . (C . c

C . (ii * c

ii . (C . (ii * c

(C . ii) * (C . c

ii . ((C . ii) * (C . c

1_ UN is Element of the carrier of UN

(ii * C) . (1_ UN) is Element of the carrier of aa

C . (1_ UN) is Element of the carrier of a

ii . (C . (1_ UN)) is Element of the carrier of aa

1_ a is Element of the carrier of a

ii . (1_ a) is Element of the carrier of aa

1_ aa is Element of the carrier of aa

UN is ()

the of UN is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr

the of UN is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr

the of UN is V1() V4( the carrier of the of UN) V5( the carrier of the of UN) V6() non empty total V28( the carrier of the of UN, the carrier of the of UN) Element of bool [: the carrier of the of UN, the carrier of the of UN:]

the carrier of the of UN is non empty set

the carrier of the of UN is non empty set

[: the carrier of the of UN, the carrier of the of UN:] is set

bool [: the carrier of the of UN, the carrier of the of UN:] is set

UN is non empty doubleLoopStr

id UN is V1() V4( the carrier of UN) V5( the carrier of UN) V6() non empty total V28( the carrier of UN, the carrier of UN) additive Element of bool [: the carrier of UN, the carrier of UN:]

the carrier of UN is non empty set

[: the carrier of UN, the carrier of UN:] is set

bool [: the carrier of UN, the carrier of UN:] is set

id the carrier of UN is V1() V4( the carrier of UN) V5( the carrier of UN) non empty total V28( the carrier of UN, the carrier of UN) Element of bool [: the carrier of UN, the carrier of UN:]

aa is Element of the carrier of UN

C is Element of the carrier of UN

aa * C is Element of the carrier of UN

(id UN) . (aa * C) is Element of the carrier of UN

(id UN) . aa is Element of the carrier of UN

(id UN) . C is Element of the carrier of UN

((id UN) . aa) * ((id UN) . C) is Element of the carrier of UN

1_ UN is Element of the carrier of UN

(id UN) . (1_ UN) is Element of the carrier of UN

UN is non empty doubleLoopStr

id UN is V1() V4( the carrier of UN) V5( the carrier of UN) V6() non empty total V28( the carrier of UN, the carrier of UN) additive Element of bool [: the carrier of UN, the carrier of UN:]

the carrier of UN is non empty set

[: the carrier of UN, the carrier of UN:] is set

bool [: the carrier of UN, the carrier of UN:] is set

id the carrier of UN is V1() V4( the carrier of UN) V5( the carrier of UN) non empty total V28( the carrier of UN, the carrier of UN) Element of bool [: the carrier of UN, the carrier of UN:]

the non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr

id the non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr is V1() V4( the carrier of the non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr ) V5( the carrier of the non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr ) V6() non empty total V28( the carrier of the non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr , the carrier of the non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr ) unity-preserving multiplicative additive ( the non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr , the non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr ) Element of bool [: the carrier of the non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr , the carrier of the non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr :]

the carrier of the non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr is non empty set

[: the carrier of the non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr , the carrier of the non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr :] is set

bool [: the carrier of the non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr , the carrier of the non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr :] is set

id the carrier of the non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr is V1() V4( the carrier of the non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr ) V5( the carrier of the non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr ) non empty total V28( the carrier of the non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr , the carrier of the non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr ) Element of bool [: the carrier of the non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr , the carrier of the non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr :]

( the non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr , the non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr ,(id the non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr )) is () ()

the of ( the non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr , the non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr ,(id the non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr )) is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr

the carrier of the of ( the non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr , the non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr ,(id the non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr )) is non empty set

the of ( the non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr , the non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr ,(id the non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr )) is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr

the carrier of the of ( the non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr , the non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr ,(id the non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr )) is non empty set

(( the non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr , the non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr ,(id the non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr ))) is V1() V4( the carrier of the of ( the non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr , the non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr ,(id the non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr ))) V5( the carrier of the of ( the non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr , the non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr ,(id the non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr ))) V6() non empty total V28( the carrier of the of ( the non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr , the non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr ,(id the non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr )), the carrier of the of ( the non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr , the non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr ,(id the non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr ))) Element of bool [: the carrier of the of ( the non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr , the non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr ,(id the non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr )), the carrier of the of ( the non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr , the non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr ,(id the non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr )):]

[: the carrier of the of ( the non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr , the non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr ,(id the non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr )), the carrier of the of ( the non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr , the non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr ,(id the non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr )):] is set

bool [: the carrier of the of ( the non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr , the non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr ,(id the non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr )), the carrier of the of ( the non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr , the non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr ,(id the non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr )):] is set

the of ( the non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr , the non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr ,(id the non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr )) is V1() V4( the carrier of the of ( the non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr , the non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr ,(id the non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr ))) V5( the carrier of the of ( the non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr , the non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr ,(id the non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr ))) V6() non empty total V28( the carrier of the of ( the non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr , the non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr ,(id the non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr )), the carrier of the of ( the non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr , the non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr ,(id the non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr ))) Element of bool [: the carrier of the of ( the non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr , the non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr ,(id the non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr )), the carrier of the of ( the non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr , the non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr ,(id the non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr )):]

UN is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr

id UN is V1() V4( the carrier of UN) V5( the carrier of UN) V6() non empty total V28( the carrier of UN, the carrier of UN) unity-preserving multiplicative additive (UN,UN) Element of bool [: the carrier of UN, the carrier of UN:]

the carrier of UN is non empty set

[: the carrier of UN, the carrier of UN:] is set

bool [: the carrier of UN, the carrier of UN:] is set

id the carrier of UN is V1() V4( the carrier of UN) V5( the carrier of UN) non empty total V28( the carrier of UN, the carrier of UN) Element of bool [: the carrier of UN, the carrier of UN:]

(UN,UN,(id UN)) is () ()

the of (UN,UN,(id UN)) is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr

the carrier of the of (UN,UN,(id UN)) is non empty set

the of (UN,UN,(id UN)) is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr

the carrier of the of (UN,UN,(id UN)) is non empty set

((UN,UN,(id UN))) is V1() V4( the carrier of the of (UN,UN,(id UN))) V5( the carrier of the of (UN,UN,(id UN))) V6() non empty total V28( the carrier of the of (UN,UN,(id UN)), the carrier of the of (UN,UN,(id UN))) Element of bool [: the carrier of the of (UN,UN,(id UN)), the carrier of the of (UN,UN,(id UN)):]

[: the carrier of the of (UN,UN,(id UN)), the carrier of the of (UN,UN,(id UN)):] is set

bool [: the carrier of the of (UN,UN,(id UN)), the carrier of the of (UN,UN,(id UN)):] is set

the of (UN,UN,(id UN)) is V1() V4( the carrier of the of (UN,UN,(id UN))) V5( the carrier of the of (UN,UN,(id UN))) V6() non empty total V28( the carrier of the of (UN,UN,(id UN)), the carrier of the of (UN,UN,(id UN))) Element of bool [: the carrier of the of (UN,UN,(id UN)), the carrier of the of (UN,UN,(id UN)):]

UN is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr

(UN) is () ()

id UN is V1() V4( the carrier of UN) V5( the carrier of UN) V6() non empty total V28( the carrier of UN, the carrier of UN) unity-preserving multiplicative additive (UN,UN) Element of bool [: the carrier of UN, the carrier of UN:]

the carrier of UN is non empty set

[: the carrier of UN, the carrier of UN:] is set

bool [: the carrier of UN, the carrier of UN:] is set

id the carrier of UN is V1() V4( the carrier of UN) V5( the carrier of UN) non empty total V28( the carrier of UN, the carrier of UN) Element of bool [: the carrier of UN, the carrier of UN:]

(UN,UN,(id UN)) is () ()

aa is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr

(aa) is () () ()

id aa is V1() V4( the carrier of aa) V5( the carrier of aa) V6() non empty total V28( the carrier of aa, the carrier of aa) unity-preserving multiplicative additive (aa,aa) Element of bool [: the carrier of aa, the carrier of aa:]

the carrier of aa is non empty set

[: the carrier of aa, the carrier of aa:] is set

bool [: the carrier of aa, the carrier of aa:] is set

id the carrier of aa is V1() V4( the carrier of aa) V5( the carrier of aa) non empty total V28( the carrier of aa, the carrier of aa) Element of bool [: the carrier of aa, the carrier of aa:]

(aa,aa,(id aa)) is () ()

((aa)) is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr

the of (aa) is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr

((aa)) is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr

the of (aa) is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr

UN is () ()

the of UN is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr

the of UN is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr

the of UN is V1() V4( the carrier of the of UN) V5( the carrier of the of UN) V6() non empty total V28( the carrier of the of UN, the carrier of the of UN) Element of bool [: the carrier of the of UN, the carrier of the of UN:]

the carrier of the of UN is non empty set

the carrier of the of UN is non empty set

[: the carrier of the of UN, the carrier of the of UN:] is set

bool [: the carrier of the of UN, the carrier of the of UN:] is set

( the of UN, the of UN, the of UN) is () ()

(UN) is V1() V4( the carrier of the of UN) V5( the carrier of the of UN) V6() non empty total V28( the carrier of the of UN, the carrier of the of UN) Element of bool [: the carrier of the of UN, the carrier of the of UN:]

the of ( the of UN, the of UN, the of UN) is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr

the carrier of the of ( the of UN, the of UN, the of UN) is non empty set

the of ( the of UN, the of UN, the of UN) is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr

the carrier of the of ( the of UN, the of UN, the of UN) is non empty set

(( the of UN, the of UN, the of UN)) is V1() V4( the carrier of the of ( the of UN, the of UN, the of UN)) V5( the carrier of the of ( the of UN, the of UN, the of UN)) V6() non empty total V28( the carrier of the of ( the of UN, the of UN, the of UN), the carrier of the of ( the of UN, the of UN, the of UN)) Element of bool [: the carrier of the of ( the of UN, the of UN, the of UN), the carrier of the of ( the of UN, the of UN, the of UN):]

[: the carrier of the of ( the of UN, the of UN, the of UN), the carrier of the of ( the of UN, the of UN, the of UN):] is set

bool [: the carrier of the of ( the of UN, the of UN, the of UN), the carrier of the of ( the of UN, the of UN, the of UN):] is set

the of ( the of UN, the of UN, the of UN) is V1() V4( the carrier of the of ( the of UN, the of UN, the of UN)) V5( the carrier of the of ( the of UN, the of UN, the of UN)) V6() non empty total V28( the carrier of the of ( the of UN, the of UN, the of UN), the carrier of the of ( the of UN, the of UN, the of UN)) Element of bool [: the carrier of the of ( the of UN, the of UN, the of UN), the carrier of the of ( the of UN, the of UN, the of UN):]

aa is Element of the carrier of the of ( the of UN, the of UN, the of UN)

C is Element of the carrier of the of ( the of UN, the of UN, the of UN)

aa + C is Element of the carrier of the of ( the of UN, the of UN, the of UN)

(( the of UN, the of UN, the of UN)) . (aa + C) is Element of the carrier of the of ( the of UN, the of UN, the of UN)

(( the of UN, the of UN, the of UN)) . aa is Element of the carrier of the of ( the of UN, the of UN, the of UN)

(( the of UN, the of UN, the of UN)) . C is Element of the carrier of the of ( the of UN, the of UN, the of UN)

((( the of UN, the of UN, the of UN)) . aa) + ((( the of UN, the of UN, the of UN)) . C) is Element of the carrier of the of ( the of UN, the of UN, the of UN)

aa is Element of the carrier of the of ( the of UN, the of UN, the of UN)

C is Element of the carrier of the of ( the of UN, the of UN, the of UN)

aa * C is Element of the carrier of the of ( the of UN, the of UN, the of UN)

(( the of UN, the of UN, the of UN)) . (aa * C) is Element of the carrier of the of ( the of UN, the of UN, the of UN)

(( the of UN, the of UN, the of UN)) . aa is Element of the carrier of the of ( the of UN, the of UN, the of UN)

(( the of UN, the of UN, the of UN)) . C is Element of the carrier of the of ( the of UN, the of UN, the of UN)

((( the of UN, the of UN, the of UN)) . aa) * ((( the of UN, the of UN, the of UN)) . C) is Element of the carrier of the of ( the of UN, the of UN, the of UN)

UN is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr

a is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr

aa is () ()

(aa) is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr

the of aa is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr

(aa) is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr

the of aa is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr

the of aa is V1() V4( the carrier of the of aa) V5( the carrier of the of aa) V6() non empty total V28( the carrier of the of aa, the carrier of the of aa) Element of bool [: the carrier of the of aa, the carrier of the of aa:]

the carrier of the of aa is non empty set

the carrier of the of aa is non empty set

[: the carrier of the of aa, the carrier of the of aa:] is set

bool [: the carrier of the of aa, the carrier of the of aa:] is set

( the of aa, the of aa, the of aa) is () ()

(( the of aa, the of aa, the of aa)) is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr

the of ( the of aa, the of aa, the of aa) is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr

(( the of aa, the of aa, the of aa)) is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr

the of ( the of aa, the of aa, the of aa) is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr

UN is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr

a is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr

the () () (UN,a) is () () (UN,a)

UN is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr

(UN) is () () ()

id UN is V1() V4( the carrier of UN) V5( the carrier of UN) V6() non empty total V28( the carrier of UN, the carrier of UN) unity-preserving multiplicative additive (UN,UN) Element of bool [: the carrier of UN, the carrier of UN:]

the carrier of UN is non empty set

[: the carrier of UN, the carrier of UN:] is set

bool [: the carrier of UN, the carrier of UN:] is set

id the carrier of UN is V1() V4( the carrier of UN) V5( the carrier of UN) non empty total V28( the carrier of UN, the carrier of UN) Element of bool [: the carrier of UN, the carrier of UN:]

(UN,UN,(id UN)) is () ()

((UN)) is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr

the of (UN) is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr

((UN)) is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr

the of (UN) is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr

UN is () ()

the of UN is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr

the of UN is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr

the of UN is V1() V4( the carrier of the of UN) V5( the carrier of the of UN) V6() non empty total V28( the carrier of the of UN, the carrier of the of UN) Element of bool [: the carrier of the of UN, the carrier of the of UN:]

the carrier of the of UN is non empty set

the carrier of the of UN is non empty set

[: the carrier of the of UN, the carrier of the of UN:] is set

bool [: the carrier of the of UN, the carrier of the of UN:] is set

(UN) is V1() V4( the carrier of the of UN) V5( the carrier of the of UN) V6() non empty total V28( the carrier of the of UN, the carrier of the of UN) Element of bool [: the carrier of the of UN, the carrier of the of UN:]

UN is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr

a is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr

aa is () ()

(aa) is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr

the of aa is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr

(aa) is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr

the of aa is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr

(aa) is V1() V4( the carrier of the of aa) V5( the carrier of the of aa) V6() non empty total V28( the carrier of the of aa, the carrier of the of aa) Element of bool [: the carrier of the of aa, the carrier of the of aa:]

the carrier of the of aa is non empty set

the carrier of the of aa is non empty set

[: the carrier of the of aa, the carrier of the of aa:] is set

bool [: the carrier of the of aa, the carrier of the of aa:] is set

the of aa is V1() V4( the carrier of the of aa) V5( the carrier of the of aa) V6() non empty total V28( the carrier of the of aa, the carrier of the of aa) Element of bool [: the carrier of the of aa, the carrier of the of aa:]

C is () ()

(C) is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr

the of C is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr

UN is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr

the carrier of UN is non empty set

a is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr

the carrier of a is non empty set

[: the carrier of UN, the carrier of a:] is set

bool [: the carrier of UN, the carrier of a:] is set

aa is V1() V4( the carrier of UN) V5( the carrier of a) V6() non empty total V28( the carrier of UN, the carrier of a) Element of bool [: the carrier of UN, the carrier of a:]

(UN,a,aa) is () ()

the of (UN,a,aa) is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr

the carrier of the of (UN,a,aa) is non empty set

the of (UN,a,aa) is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr

the carrier of the of (UN,a,aa) is non empty set

((UN,a,aa)) is V1() V4( the carrier of the of (UN,a,aa)) V5( the carrier of the of (UN,a,aa)) V6() non empty total V28( the carrier of the of (UN,a,aa), the carrier of the of (UN,a,aa)) Element of bool [: the carrier of the of (UN,a,aa), the carrier of the of (UN,a,aa):]

[: the carrier of the of (UN,a,aa), the carrier of the of (UN,a,aa):] is set

bool [: the carrier of the of (UN,a,aa), the carrier of the of (UN,a,aa):] is set

the of (UN,a,aa) is V1() V4( the carrier of the of (UN,a,aa)) V5( the carrier of the of (UN,a,aa)) V6() non empty total V28( the carrier of the of (UN,a,aa), the carrier of the of (UN,a,aa)) Element of bool [: the carrier of the of (UN,a,aa), the carrier of the of (UN,a,aa):]

((UN,a,aa)) is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr

((UN,a,aa)) is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr

UN is () ()

(UN) is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr

the of UN is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr

(UN) is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr

the of UN is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr

the of UN is V1() V4( the carrier of the of UN) V5( the carrier of the of UN) V6() non empty total V28( the carrier of the of UN, the carrier of the of UN) Element of bool [: the carrier of the of UN, the carrier of the of UN:]

the carrier of the of UN is non empty set

the carrier of the of UN is non empty set

[: the carrier of the of UN, the carrier of the of UN:] is set

bool [: the carrier of the of UN, the carrier of the of UN:] is set

( the of UN, the of UN, the of UN) is () ()

a is () ()

(a) is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr

the of a is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr

(a) is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr

the of a is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr

UN is () ()

(UN) is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr

the of UN is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr

a is () ()

(a) is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr

the of a is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr

the of UN is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr

the of UN is V1() V4( the carrier of the of UN) V5( the carrier of the of UN) V6() non empty total V28( the carrier of the of UN, the carrier of the of UN) Element of bool [: the carrier of the of UN, the carrier of the of UN:]

the carrier of the of UN is non empty set

the carrier of the of UN is non empty set

[: the carrier of the of UN, the carrier of the of UN:] is set

bool [: the carrier of the of UN, the carrier of the of UN:] is set

( the of UN, the of UN, the of UN) is () ()

the of a is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr

the of a is V1() V4( the carrier of the of a) V5( the carrier of the of a) V6() non empty total V28( the carrier of the of a, the carrier of the of a) Element of bool [: the carrier of the of a, the carrier of the of a:]

the carrier of the of a is non empty set

the carrier of the of a is non empty set

[: the carrier of the of a, the carrier of the of a:] is set

bool [: the carrier of the of a, the carrier of the of a:] is set

( the of a, the of a, the of a) is () ()

(UN) is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr

(a) is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr

aa is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr

C is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr

ii is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr

ia is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr

UN is () () ()

(UN) is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr

the of UN is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr

(UN) is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr

the of UN is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr

a is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr

aa is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr

UN is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr

the carrier of UN is non empty set

a is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr

the carrier of a is non empty set

[: the carrier of UN, the carrier of a:] is set

bool [: the carrier of UN, the carrier of a:] is set

aa is () () (UN,a)

the of aa is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr

(aa) is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr

the of aa is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr

(aa) is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr

the of aa is V1() V4( the carrier of the of aa) V5( the carrier of the of aa) V6() non empty total V28( the carrier of the of aa, the carrier of the of aa) Element of bool [: the carrier of the of aa, the carrier of the of aa:]

the carrier of the of aa is non empty set

the carrier of the of aa is non empty set

[: the carrier of the of aa, the carrier of the of aa:] is set

bool [: the carrier of the of aa, the carrier of the of aa:] is set

C is V1() V4( the carrier of UN) V5( the carrier of a) V6() non empty total V28( the carrier of UN, the carrier of a) Element of bool [: the carrier of UN, the carrier of a:]

(UN,a,C) is () ()

UN is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr

the carrier of UN is non empty set

a is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr

the carrier of a is non empty set

[: the carrier of UN, the carrier of a:] is set

bool [: the carrier of UN, the carrier of a:] is set

aa is () () (UN,a)

C is V1() V4( the carrier of UN) V5( the carrier of a) V6() non empty total V28( the carrier of UN, the carrier of a) Element of bool [: the carrier of UN, the carrier of a:]

(UN,a,C) is () ()

UN is () () ()

(UN) is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr

the of UN is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr

(UN) is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr

the of UN is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr

a is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr

aa is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr

the carrier of a is non empty set

the carrier of aa is non empty set

[: the carrier of a, the carrier of aa:] is set

bool [: the carrier of a, the carrier of aa:] is set

C is () () (a,aa)

ii is V1() V4( the carrier of a) V5( the carrier of aa) V6() non empty total V28( the carrier of a, the carrier of aa) Element of bool [: the carrier of a, the carrier of aa:]

(a,aa,ii) is () ()

UN is () ()

(UN) is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr

the of UN is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr

a is () ()

(a) is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr

the of a is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr

the of UN is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr

the of UN is V1() V4( the carrier of the of UN) V5( the carrier of the of UN) V6() non empty total V28( the carrier of the of UN, the carrier of the of UN) Element of bool [: the carrier of the of UN, the carrier of the of UN:]

the carrier of the of UN is non empty set

the carrier of the of UN is non empty set

[: the carrier of the of UN, the carrier of the of UN:] is set

bool [: the carrier of the of UN, the carrier of the of UN:] is set

( the of UN, the of UN, the of UN) is () ()

the of a is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr

the of a is V1() V4( the carrier of the of a) V5( the carrier of the of a) V6() non empty total V28( the carrier of the of a, the carrier of the of a) Element of bool [: the carrier of the of a, the carrier of the of a:]

the carrier of the of a is non empty set

the carrier of the of a is non empty set

[: the carrier of the of a, the carrier of the of a:] is set

bool [: the carrier of the of a, the carrier of the of a:] is set

( the of a, the of a, the of a) is () ()

aa is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr

C is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr

ii is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr

the carrier of C is non empty set

the carrier of ii is non empty set

[: the carrier of C, the carrier of ii:] is set

bool [: the carrier of C, the carrier of ii:] is set

ia is V1() V4( the carrier of C) V5( the carrier of ii) V6() non empty total V28( the carrier of C, the carrier of ii) Element of bool [: the carrier of C, the carrier of ii:]

(C,ii,ia) is () ()

the carrier of aa is non empty set

[: the carrier of aa, the carrier of C:] is set

bool [: the carrier of aa, the carrier of C:] is set

ii is V1() V4( the carrier of aa) V5( the carrier of C) V6() non empty total V28( the carrier of aa, the carrier of C) Element of bool [: the carrier of aa, the carrier of C:]

(aa,C,ii) is () ()

ia * ii is V1() V4( the carrier of aa) V5( the carrier of ii) V6() non empty total V28( the carrier of aa, the carrier of ii) Element of bool [: the carrier of aa, the carrier of ii:]

[: the carrier of aa, the carrier of ii:] is set

bool [: the carrier of aa, the carrier of ii:] is set

(aa,ii,(ia * ii)) is () ()

c

H1 is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr

the carrier of H1 is non empty set

f is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr

the carrier of f is non empty set

[: the carrier of H1, the carrier of f:] is set

bool [: the carrier of H1, the carrier of f:] is set

G1 is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr

the carrier of G1 is non empty set

[: the carrier of G1, the carrier of H1:] is set

bool [: the carrier of G1, the carrier of H1:] is set

f is V1() V4( the carrier of H1) V5( the carrier of f) V6() non empty total V28( the carrier of H1, the carrier of f) Element of bool [: the carrier of H1, the carrier of f:]

(H1,f,f) is () ()

G is V1() V4( the carrier of G1) V5( the carrier of H1) V6() non empty total V28( the carrier of G1, the carrier of H1) Element of bool [: the carrier of G1, the carrier of H1:]

(G1,H1,G) is () ()

f * G is V1() V4( the carrier of G1) V5( the carrier of f) V6() non empty total V28( the carrier of G1, the carrier of f) Element of bool [: the carrier of G1, the carrier of f:]

[: the carrier of G1, the carrier of f:] is set

bool [: the carrier of G1, the carrier of f:] is set

(G1,f,(f * G)) is () ()

(a) is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr

aa is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr

C is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr

ia is () () ()

ii is () () ()

(UN) is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr

c

G1 is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr

ii is () () (aa,C)

the carrier of aa is non empty set

the carrier of c

[: the carrier of aa, the carrier of c

bool [: the carrier of aa, the carrier of c

H1 is () () (aa,c

f is V1() V4( the carrier of aa) V5( the carrier of c

(aa,c

the carrier of G1 is non empty set

[: the carrier of c

bool [: the carrier of c

f is () () (c

G is V1() V4( the carrier of c

(c

G * f is V1() V4( the carrier of aa) V5( the carrier of G1) V6() non empty total V28( the carrier of aa, the carrier of G1) Element of bool [: the carrier of aa, the carrier of G1:]

[: the carrier of aa, the carrier of G1:] is set

bool [: the carrier of aa, the carrier of G1:] is set

(aa,G1,(G * f)) is () ()

UN is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr

a is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr

aa is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr

C is () ()

(C) is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr

the of C is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr

(C) is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr

the of C is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr

the of C is V1() V4( the carrier of the of C) V5( the carrier of the of C) V6() non empty total V28( the carrier of the of C, the carrier of the of C) Element of bool [: the carrier of the of C, the carrier of the of C:]

the carrier of the of C is non empty set

the carrier of the of C is non empty set

[: the carrier of the of C, the carrier of the of C:] is set

bool [: the carrier of the of C, the carrier of the of C:] is set

( the of C, the of C, the of C) is () ()

ii is () ()

(ii) is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr

the of ii is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr

(ii) is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr

the of ii is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr

the carrier of UN is non empty set

the carrier of a is non empty set

[: the carrier of UN, the carrier of a:] is set

bool [: the carrier of UN, the carrier of a:] is set

ia is () () (UN,a)

ii is V1() V4( the carrier of UN) V5( the carrier of a) V6() non empty total V28( the carrier of UN, the carrier of a) Element of bool [: the carrier of UN, the carrier of a:]

(UN,a,ii) is () ()

c

(c

the of c

(c

the of c

the of c

the carrier of the of c

the carrier of the of c

[: the carrier of the of c

bool [: the carrier of the of c

( the of c

G1 is () ()

(G1) is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr

the of G1 is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr

(G1) is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr

the of G1 is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr

the carrier of aa is non empty set

[: the carrier of a, the carrier of aa:] is set

bool [: the carrier of a, the carrier of aa:] is set

H1 is () () (a,aa)

f is V1() V4( the carrier of a) V5( the carrier of aa) V6() non empty total V28( the carrier of a, the carrier of aa) Element of bool [: the carrier of a, the carrier of aa:]

(a,aa,f) is () ()

(G1,ii) is () () ()

f * ii is V1() V4( the carrier of UN) V5( the carrier of aa) V6() non empty total V28( the carrier of UN, the carrier of aa) Element of bool [: the carrier of UN, the carrier of aa:]

[: the carrier of UN, the carrier of aa:] is set

bool [: the carrier of UN, the carrier of aa:] is set

(UN,aa,(f * ii)) is () ()

((G1,ii)) is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr

the of (G1,ii) is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr

((G1,ii)) is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr

the of (G1,ii) is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr

UN is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr

a is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr

aa is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr

C is () () (UN,a)

ii is () () (aa,UN)

(C,ii) is () () ()

the carrier of UN is non empty set

the carrier of a is non empty set

[: the carrier of UN, the carrier of a:] is set

bool [: the carrier of UN, the carrier of a:] is set

ia is V1() V4( the carrier of UN) V5( the carrier of a) V6() non empty total V28( the carrier of UN, the carrier of a) Element of bool [: the carrier of UN, the carrier of a:]

(UN,a,ia) is () ()

the carrier of aa is non empty set

[: the carrier of aa, the carrier of UN:] is set

bool [: the carrier of aa, the carrier of UN:] is set

ii is V1() V4( the carrier of aa) V5( the carrier of UN) V6() non empty total V28( the carrier of aa, the carrier of UN) Element of bool [: the carrier of aa, the carrier of UN:]

(aa,UN,ii) is () ()

(C) is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr

the of C is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr

(ii) is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr

the of ii is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr

ia * ii is V1() V4( the carrier of aa) V5( the carrier of a) V6() non empty total V28( the carrier of aa, the carrier of a) Element of bool [: the carrier of aa, the carrier of a:]

[: the carrier of aa, the carrier of a:] is set

bool [: the carrier of aa, the carrier of a:] is set

(aa,a,(ia * ii)) is () ()

((C,ii)) is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr

the of (C,ii) is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr

((C,ii)) is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr

the of (C,ii) is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr

a is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr

aa is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr

UN is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr

C is () () (a,aa)

ii is () () (UN,a)

(C,ii) is () () ()

a is () () ()

(a) is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr

the of a is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr

UN is () () ()

(UN) is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr

the of UN is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr

(a,UN) is () () ()

(UN) is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr

the of UN is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr

(a) is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr

the of a is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr

the carrier of (UN) is non empty set

the carrier of (a) is non empty set

[: the carrier of (UN), the carrier of (a):] is set

bool [: the carrier of (UN), the carrier of (a):] is set

ia is () () ((UN),(a))

ii is V1() V4( the carrier of (UN)) V5( the carrier of (a)) V6() non empty total V28( the carrier of (UN), the carrier of (a)) Element of bool [: the carrier of (UN), the carrier of (a):]

((UN),(a),ii) is () ()

the carrier of (UN) is non empty set

[: the carrier of (UN), the carrier of (UN):] is set

bool [: the carrier of (UN), the carrier of (UN):] is set

c

G1 is V1() V4( the carrier of (UN)) V5( the carrier of (UN)) V6() non empty total V28( the carrier of (UN), the carrier of (UN)) Element of bool [: the carrier of (UN), the carrier of (UN):]

((UN),(UN),G1) is () ()

ii * G1 is V1() V4( the carrier of (UN)) V5( the carrier of (a)) V6() non empty total V28( the carrier of (UN), the carrier of (a)) Element of bool [: the carrier of (UN), the carrier of (a):]

[: the carrier of (UN), the carrier of (a):] is set

bool [: the carrier of (UN), the carrier of (a):] is set

((UN),(a),(ii * G1)) is () ()

a is () () ()

(a) is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr

the of a is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr

UN is () () ()

(UN) is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr

the of UN is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr

(a,UN) is () () ()

((a,UN)) is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr

the of (a,UN) is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr

(UN) is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr

the of UN is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr

((a,UN)) is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr

the of (a,UN) is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr

(a) is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr

the of a is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr

aa is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr

the carrier of aa is non empty set

C is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr

the carrier of C is non empty set

[: the carrier of aa, the carrier of C:] is set

bool [: the carrier of aa, the carrier of C:] is set

ii is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr

the carrier of ii is non empty set

[: the carrier of C, the carrier of ii:] is set

bool [: the carrier of C, the carrier of ii:] is set

ia is V1() V4( the carrier of aa) V5( the carrier of C) V6() non empty total V28( the carrier of aa, the carrier of C) Element of bool [: the carrier of aa, the carrier of C:]

(aa,C,ia) is () ()

ii is V1() V4( the carrier of C) V5( the carrier of ii) V6() non empty total V28( the carrier of C, the carrier of ii) Element of bool [: the carrier of C, the carrier of ii:]

(C,ii,ii) is () ()

ii * ia is V1() V4( the carrier of aa) V5( the carrier of ii) V6() non empty total V28( the carrier of aa, the carrier of ii) Element of bool [: the carrier of aa, the carrier of ii:]

[: the carrier of aa, the carrier of ii:] is set

bool [: the carrier of aa, the carrier of ii:] is set

(aa,ii,(ii * ia)) is () ()

aa is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr

the carrier of aa is non empty set

C is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr

the carrier of C is non empty set

[: the carrier of aa, the carrier of C:] is set

bool [: the carrier of aa, the carrier of C:] is set

ii is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr

the carrier of ii is non empty set

[: the carrier of C, the carrier of ii:] is set

bool [: the carrier of C, the carrier of ii:] is set

ia is V1() V4( the carrier of aa) V5( the carrier of C) V6() non empty total V28( the carrier of aa, the carrier of C) Element of bool [: the carrier of aa, the carrier of C:]

(aa,C,ia) is () ()

ii is V1() V4( the carrier of C) V5( the carrier of ii) V6() non empty total V28( the carrier of C, the carrier of ii) Element of bool [: the carrier of C, the carrier of ii:]

(C,ii,ii) is () ()

ii * ia is V1() V4( the carrier of aa) V5( the carrier of ii) V6() non empty total V28( the carrier of aa, the carrier of ii) Element of bool [: the carrier of aa, the carrier of ii:]

[: the carrier of aa, the carrier of ii:] is set

bool [: the carrier of aa, the carrier of ii:] is set

(aa,ii,(ii * ia)) is () ()

UN is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr

a is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr

aa is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr

C is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr

ii is () () (UN,a)

ia is () () (a,aa)

(ia,ii) is () () ()

ii is () () (aa,C)

(ii,(ia,ii)) is () () ()

(ii,ia) is () () ()

((ii,ia),ii) is () () ()

the carrier of UN is non empty set

the carrier of a is non empty set

[: the carrier of UN, the carrier of a:] is set

bool [: the carrier of UN, the carrier of a:] is set

c

(UN,a,c

the carrier of aa is non empty set

the carrier of C is non empty set

[: the carrier of aa, the carrier of C:] is set

bool [: the carrier of aa, the carrier of C:] is set

G1 is V1() V4( the carrier of aa) V5( the carrier of C) V6() non empty total V28( the carrier of aa, the carrier of C) Element of bool [: the carrier of aa, the carrier of C:]

(aa,C,G1) is () ()

[: the carrier of a, the carrier of aa:] is set

bool [: the carrier of a, the carrier of aa:] is set

H1 is V1() V4( the carrier of a) V5( the carrier of aa) V6() non empty total V28( the carrier of a, the carrier of aa) Element of bool [: the carrier of a, the carrier of aa:]

(a,aa,H1) is () ()

(ia) is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr

the of ia is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr

(ii) is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr

the of ii is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr

G1 * H1 is V1() V4( the carrier of a) V5( the carrier of C) V6() non empty total V28( the carrier of a, the carrier of C) Element of bool [: the carrier of a, the carrier of C:]

[: the carrier of a, the carrier of C:] is set

bool [: the carrier of a, the carrier of C:] is set

(a,C,(G1 * H1)) is () ()

(ia) is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr

the of ia is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr

((ii,ia)) is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr

the of (ii,ia) is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr

(ii) is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr

the of ii is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr

((ia,ii)) is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr

the of (ia,ii) is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr

H1 * c

[: the carrier of UN, the carrier of aa:] is set

bool [: the carrier of UN, the carrier of aa:] is set

(UN,aa,(H1 * c

G1 * (H1 * c

[: the carrier of UN, the carrier of C:] is set

bool [: the carrier of UN, the carrier of C:] is set

(UN,C,(G1 * (H1 * c

(G1 * H1) * c

(UN,C,((G1 * H1) * c

aa is () () ()

(aa) is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr

the of aa is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr

a is () () ()

(a) is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr

the of a is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr

(a) is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr

the of a is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr

UN is () () ()

(UN) is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr

the of UN is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr

(a,UN) is () () ()

(aa,(a,UN)) is () () ()

(aa,a) is () () ()

((aa,a),UN) is () () ()

(UN) is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr

the of UN is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr

(aa) is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr

the of aa is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr

c

H1 is () () ((UN),(a))

G1 is () () ((UN),(UN))

(H1,G1) is () () ()

(c

(c

((c

UN is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr

(UN) is () () (UN,UN)

id UN is V1() V4( the carrier of UN) V5( the carrier of UN) V6() non empty total V28( the carrier of UN, the carrier of UN) unity-preserving multiplicative additive (UN,UN) Element of bool [: the carrier of UN, the carrier of UN:]

the carrier of UN is non empty set

[: the carrier of UN, the carrier of UN:] is set

bool [: the carrier of UN, the carrier of UN:] is set

id the carrier of UN is V1() V4( the carrier of UN) V5( the carrier of UN) non empty total V28( the carrier of UN, the carrier of UN) Element of bool [: the carrier of UN, the carrier of UN:]

(UN,UN,(id UN)) is () ()

((UN)) is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr

the of (UN) is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr

((UN)) is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr

the of (UN) is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr

aa is () () ()

(aa) is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr

the of aa is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr

((UN),aa) is () () ()

(aa) is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr

the of aa is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr

the carrier of (aa) is non empty set

[: the carrier of (aa), the carrier of UN:] is set

bool [: the carrier of (aa), the carrier of UN:] is set

ii is () () ((aa),UN)

ia is V1() V4( the carrier of (aa)) V5( the carrier of UN) V6() non empty total V28( the carrier of (aa), the carrier of UN) Element of bool [: the carrier of (aa), the carrier of UN:]

((aa),UN,ia) is () ()

(id UN) * ia is V1() V4( the carrier of (aa)) V5( the carrier of UN) V6() non empty total V28( the carrier of (aa), the carrier of UN) Element of bool [: the carrier of (aa), the carrier of UN:]

aa is () () ()

(aa) is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr

the of aa is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr

(aa,(UN)) is () () ()

(aa) is non empty right_complementable V96() V97() V98() unital associative right-distributive left-distributive right_unital well-unital V148() left_unital doubleLoopStr

the of aa is non empty right_complementable V96() V97() V98() unital associative