:: DIRORT semantic presentation

K75() is M2(K24(K71()))

K71() is set

K24(K71()) is set

K70() is set

K24(K70()) is set

K24(K75()) is set

AS is non empty AffinStruct

the carrier of AS is set

AS is non empty V67() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct

the carrier of AS is set

u is M2( the carrier of AS)

u1 is M2( the carrier of AS)

CESpace (AS,u,u1) is non empty strict AffinStruct

the carrier of (CESpace (AS,u,u1)) is set

CORTE (AS,u,u1) is M2(K24(K25(K25( the carrier of AS, the carrier of AS),K25( the carrier of AS, the carrier of AS))))

K25( the carrier of AS, the carrier of AS) is set

K25(K25( the carrier of AS, the carrier of AS),K25( the carrier of AS, the carrier of AS)) is set

K24(K25(K25( the carrier of AS, the carrier of AS),K25( the carrier of AS, the carrier of AS))) is set

AffinStruct(# the carrier of AS,(CORTE (AS,u,u1)) #) is strict AffinStruct

v is M2( the carrier of (CESpace (AS,u,u1)))

v2 is M2( the carrier of (CESpace (AS,u,u1)))

w1 is M2( the carrier of (CESpace (AS,u,u1)))

v1 is M2( the carrier of (CESpace (AS,u,u1)))

w is M2( the carrier of (CESpace (AS,u,u1)))

w is M2( the carrier of AS)

w1 is M2( the carrier of AS)

w1 is M2( the carrier of AS)

u9 is M2( the carrier of AS)

v9 is M2( the carrier of AS)

v2 is M2( the carrier of (CESpace (AS,u,u1)))

v is M2( the carrier of (CESpace (AS,u,u1)))

v1 is M2( the carrier of (CESpace (AS,u,u1)))

w is M2( the carrier of AS)

w is M2( the carrier of AS)

w1 is M2( the carrier of AS)

w1 is M2( the carrier of AS)

w1 is M2( the carrier of (CESpace (AS,u,u1)))

v2 is M2( the carrier of (CESpace (AS,u,u1)))

v is M2( the carrier of (CESpace (AS,u,u1)))

v1 is M2( the carrier of (CESpace (AS,u,u1)))

w is M2( the carrier of AS)

w is M2( the carrier of AS)

w1 is M2( the carrier of AS)

w1 is M2( the carrier of AS)

w1 is M2( the carrier of (CESpace (AS,u,u1)))

AS is non empty V67() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct

the carrier of AS is set

u is M2( the carrier of AS)

u1 is M2( the carrier of AS)

CMSpace (AS,u,u1) is non empty strict AffinStruct

the carrier of (CMSpace (AS,u,u1)) is set

CORTM (AS,u,u1) is M2(K24(K25(K25( the carrier of AS, the carrier of AS),K25( the carrier of AS, the carrier of AS))))

K25( the carrier of AS, the carrier of AS) is set

K25(K25( the carrier of AS, the carrier of AS),K25( the carrier of AS, the carrier of AS)) is set

K24(K25(K25( the carrier of AS, the carrier of AS),K25( the carrier of AS, the carrier of AS))) is set

AffinStruct(# the carrier of AS,(CORTM (AS,u,u1)) #) is strict AffinStruct

v is M2( the carrier of (CMSpace (AS,u,u1)))

v2 is M2( the carrier of (CMSpace (AS,u,u1)))

w1 is M2( the carrier of (CMSpace (AS,u,u1)))

v1 is M2( the carrier of (CMSpace (AS,u,u1)))

w is M2( the carrier of (CMSpace (AS,u,u1)))

w is M2( the carrier of AS)

w1 is M2( the carrier of AS)

w1 is M2( the carrier of AS)

u9 is M2( the carrier of AS)

v9 is M2( the carrier of AS)

v2 is M2( the carrier of (CMSpace (AS,u,u1)))

v is M2( the carrier of (CMSpace (AS,u,u1)))

v1 is M2( the carrier of (CMSpace (AS,u,u1)))

w is M2( the carrier of AS)

w is M2( the carrier of AS)

w1 is M2( the carrier of AS)

w1 is M2( the carrier of AS)

w1 is M2( the carrier of (CMSpace (AS,u,u1)))

v2 is M2( the carrier of (CMSpace (AS,u,u1)))

v is M2( the carrier of (CMSpace (AS,u,u1)))

v1 is M2( the carrier of (CMSpace (AS,u,u1)))

w is M2( the carrier of AS)

w is M2( the carrier of AS)

w1 is M2( the carrier of AS)

w1 is M2( the carrier of AS)

w1 is M2( the carrier of (CMSpace (AS,u,u1)))

AS is non empty V67() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct

the carrier of AS is set

u is M2( the carrier of AS)

u1 is M2( the carrier of AS)

AS is non empty V67() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct

the carrier of AS is set

u is M2( the carrier of AS)

u1 is M2( the carrier of AS)

CESpace (AS,u,u1) is non empty strict AffinStruct

u2 is non empty strict AffinStruct

the carrier of u2 is set

v is M2( the carrier of u2)

v1 is M2( the carrier of u2)

v2 is M2( the carrier of u2)

w is M2( the carrier of u2)

w1 is M2( the carrier of u2)

w is M2( the carrier of u2)

w1 is M2( the carrier of u2)

u9 is M2( the carrier of u2)

w1 is M2( the carrier of u2)

v9 is M2( the carrier of u2)

w9 is M2( the carrier of u2)

v19 is M2( the carrier of u2)

u19 is M2( the carrier of u2)

w19 is M2( the carrier of u2)

u29 is M2( the carrier of u2)

v29 is M2( the carrier of u2)

c

c

c

c

c

c

c

c

c

c

c

c

c

c

c

c

c

c

AS is non empty V67() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct

the carrier of AS is set

u is M2( the carrier of AS)

u1 is M2( the carrier of AS)

CMSpace (AS,u,u1) is non empty strict AffinStruct

the carrier of (CMSpace (AS,u,u1)) is set

v1 is M2( the carrier of (CMSpace (AS,u,u1)))

u2 is M2( the carrier of (CMSpace (AS,u,u1)))

v is M2( the carrier of (CMSpace (AS,u,u1)))

v1 is M2( the carrier of (CMSpace (AS,u,u1)))

u2 is M2( the carrier of (CMSpace (AS,u,u1)))

v is M2( the carrier of (CMSpace (AS,u,u1)))

u2 is M2( the carrier of (CMSpace (AS,u,u1)))

v is M2( the carrier of (CMSpace (AS,u,u1)))

v1 is M2( the carrier of (CMSpace (AS,u,u1)))

v2 is M2( the carrier of (CMSpace (AS,u,u1)))

w is M2( the carrier of (CMSpace (AS,u,u1)))

w1 is M2( the carrier of (CMSpace (AS,u,u1)))

w is M2( the carrier of (CMSpace (AS,u,u1)))

w1 is M2( the carrier of (CMSpace (AS,u,u1)))

w1 is M2( the carrier of (CMSpace (AS,u,u1)))

u9 is M2( the carrier of (CMSpace (AS,u,u1)))

v9 is M2( the carrier of (CMSpace (AS,u,u1)))

u19 is M2( the carrier of (CMSpace (AS,u,u1)))

w9 is M2( the carrier of (CMSpace (AS,u,u1)))

v19 is M2( the carrier of (CMSpace (AS,u,u1)))

w19 is M2( the carrier of (CMSpace (AS,u,u1)))

u29 is M2( the carrier of (CMSpace (AS,u,u1)))

c

v29 is M2( the carrier of (CMSpace (AS,u,u1)))

c

c

c

c

c

c

c

c

c

c

AS is non empty V67() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct

the carrier of AS is set

u is M2( the carrier of AS)

u1 is M2( the carrier of AS)

CESpace (AS,u,u1) is non empty strict AffinStruct

the carrier of (CESpace (AS,u,u1)) is set

v1 is M2( the carrier of (CESpace (AS,u,u1)))

u2 is M2( the carrier of (CESpace (AS,u,u1)))

v is M2( the carrier of (CESpace (AS,u,u1)))

v1 is M2( the carrier of (CESpace (AS,u,u1)))

u2 is M2( the carrier of (CESpace (AS,u,u1)))

v is M2( the carrier of (CESpace (AS,u,u1)))

u2 is M2( the carrier of (CESpace (AS,u,u1)))

v is M2( the carrier of (CESpace (AS,u,u1)))

v1 is M2( the carrier of (CESpace (AS,u,u1)))

v2 is M2( the carrier of (CESpace (AS,u,u1)))

w is M2( the carrier of (CESpace (AS,u,u1)))

w1 is M2( the carrier of (CESpace (AS,u,u1)))

w is M2( the carrier of (CESpace (AS,u,u1)))

w1 is M2( the carrier of (CESpace (AS,u,u1)))

w1 is M2( the carrier of (CESpace (AS,u,u1)))

u9 is M2( the carrier of (CESpace (AS,u,u1)))

v9 is M2( the carrier of (CESpace (AS,u,u1)))

u19 is M2( the carrier of (CESpace (AS,u,u1)))

w9 is M2( the carrier of (CESpace (AS,u,u1)))

v19 is M2( the carrier of (CESpace (AS,u,u1)))

w19 is M2( the carrier of (CESpace (AS,u,u1)))

u29 is M2( the carrier of (CESpace (AS,u,u1)))

c

v29 is M2( the carrier of (CESpace (AS,u,u1)))

c

c

c

c

c

c

c

c

c

c

AS is non empty () AffinStruct

the carrier of AS is set

u is M2( the carrier of AS)

u1 is M2( the carrier of AS)

u2 is M2( the carrier of AS)

v is M2( the carrier of AS)

AS is non empty () AffinStruct

the carrier of AS is set

u is M2( the carrier of AS)

u1 is M2( the carrier of AS)

u2 is M2( the carrier of AS)

v is M2( the carrier of AS)

AS is non empty () AffinStruct

the carrier of AS is set

AS is non empty () AffinStruct

the carrier of AS is set

AS is non empty () AffinStruct

the carrier of AS is set

u is M2( the carrier of AS)

u1 is M2( the carrier of AS)

u2 is M2( the carrier of AS)

the M2( the carrier of AS) is M2( the carrier of AS)

v1 is M2( the carrier of AS)

AS is non empty () AffinStruct

the carrier of AS is set

u is M2( the carrier of AS)

u1 is M2( the carrier of AS)

u2 is M2( the carrier of AS)

v is M2( the carrier of AS)

v1 is M2( the carrier of AS)

v2 is M2( the carrier of AS)

AS is non empty () AffinStruct

the carrier of AS is set

u is M2( the carrier of AS)

u1 is M2( the carrier of AS)

u2 is M2( the carrier of AS)

v is M2( the carrier of AS)

v1 is M2( the carrier of AS)

v2 is M2( the carrier of AS)

AS is non empty () AffinStruct

the carrier of AS is set

u is M2( the carrier of AS)

u1 is M2( the carrier of AS)

u2 is M2( the carrier of AS)

v is M2( the carrier of AS)

v1 is M2( the carrier of AS)

v2 is M2( the carrier of AS)

w is M2( the carrier of AS)

w1 is M2( the carrier of AS)

u is M2( the carrier of AS)

u1 is M2( the carrier of AS)

u2 is M2( the carrier of AS)

v is M2( the carrier of AS)

v1 is M2( the carrier of AS)

v2 is M2( the carrier of AS)

w is M2( the carrier of AS)

w1 is M2( the carrier of AS)

u is M2( the carrier of AS)

u1 is M2( the carrier of AS)

v1 is M2( the carrier of AS)

v2 is M2( the carrier of AS)

u2 is M2( the carrier of AS)

v is M2( the carrier of AS)

w is M2( the carrier of AS)

w1 is M2( the carrier of AS)

w1 is M2( the carrier of AS)

u9 is M2( the carrier of AS)

w is M2( the carrier of AS)

w1 is M2( the carrier of AS)

AS is non empty () AffinStruct

the carrier of AS is set

u is M2( the carrier of AS)

u1 is M2( the carrier of AS)

u2 is M2( the carrier of AS)

v is M2( the carrier of AS)

v1 is M2( the carrier of AS)

v2 is M2( the carrier of AS)

w is M2( the carrier of AS)

w1 is M2( the carrier of AS)

u is M2( the carrier of AS)

u1 is M2( the carrier of AS)

u2 is M2( the carrier of AS)

v is M2( the carrier of AS)

v1 is M2( the carrier of AS)

v2 is M2( the carrier of AS)

w is M2( the carrier of AS)

w1 is M2( the carrier of AS)

u is M2( the carrier of AS)

u1 is M2( the carrier of AS)

v is M2( the carrier of AS)

v1 is M2( the carrier of AS)

u2 is M2( the carrier of AS)

v2 is M2( the carrier of AS)

w is M2( the carrier of AS)

w1 is M2( the carrier of AS)

w1 is M2( the carrier of AS)

w1 is M2( the carrier of AS)

w is M2( the carrier of AS)

u9 is M2( the carrier of AS)

AS is non empty () AffinStruct

the carrier of AS is set

u is M2( the carrier of AS)

u1 is M2( the carrier of AS)

u2 is M2( the carrier of AS)

v is M2( the carrier of AS)

v1 is M2( the carrier of AS)

v2 is M2( the carrier of AS)

w is M2( the carrier of AS)

w1 is M2( the carrier of AS)

AS is non empty V67() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct

the carrier of AS is set

u is M2( the carrier of AS)

u1 is M2( the carrier of AS)

CESpace (AS,u,u1) is non empty strict AffinStruct

u2 is non empty () AffinStruct

CORTE (AS,u,u1) is M2(K24(K25(K25( the carrier of AS, the carrier of AS),K25( the carrier of AS, the carrier of AS))))

K25( the carrier of AS, the carrier of AS) is set

K25(K25( the carrier of AS, the carrier of AS),K25( the carrier of AS, the carrier of AS)) is set

K24(K25(K25( the carrier of AS, the carrier of AS),K25( the carrier of AS, the carrier of AS))) is set

AffinStruct(# the carrier of AS,(CORTE (AS,u,u1)) #) is strict AffinStruct

the carrier of u2 is set

v is M2( the carrier of u2)

v1 is M2( the carrier of u2)

w is M2( the carrier of u2)

w1 is M2( the carrier of u2)

w1 is M2( the carrier of u2)

w1 is M2( the carrier of u2)

v2 is M2( the carrier of u2)

w is M2( the carrier of u2)

u9 is M2( the carrier of AS)

u19 is M2( the carrier of AS)

v9 is M2( the carrier of AS)

v19 is M2( the carrier of AS)

w9 is M2( the carrier of AS)

w19 is M2( the carrier of AS)

u29 is M2( the carrier of AS)

v29 is M2( the carrier of AS)

v is M2( the carrier of u2)

v1 is M2( the carrier of u2)

v2 is M2( the carrier of u2)

w is M2( the carrier of u2)

w1 is M2( the carrier of AS)

w1 is M2( the carrier of AS)

w is M2( the carrier of AS)

w1 is M2( the carrier of AS)

v is M2( the carrier of u2)

v1 is M2( the carrier of u2)

w is M2( the carrier of u2)

w1 is M2( the carrier of u2)

w1 is M2( the carrier of u2)

w1 is M2( the carrier of u2)

v2 is M2( the carrier of u2)

w is M2( the carrier of u2)

u9 is M2( the carrier of AS)

u19 is M2( the carrier of AS)

v9 is M2( the carrier of AS)

v19 is M2( the carrier of AS)

w9 is M2( the carrier of AS)

w19 is M2( the carrier of AS)

u29 is M2( the carrier of AS)

v29 is M2( the carrier of AS)

v is M2( the carrier of u2)

v1 is M2( the carrier of u2)

w is M2( the carrier of u2)

w1 is M2( the carrier of u2)

w1 is M2( the carrier of u2)

w1 is M2( the carrier of u2)

v2 is M2( the carrier of u2)

w is M2( the carrier of u2)

u9 is M2( the carrier of AS)

u19 is M2( the carrier of AS)

v9 is M2( the carrier of AS)

v19 is M2( the carrier of AS)

w9 is M2( the carrier of AS)

w19 is M2( the carrier of AS)

u29 is M2( the carrier of AS)

v29 is M2( the carrier of AS)

AS is non empty V67() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct

the carrier of AS is set

u is M2( the carrier of AS)

u1 is M2( the carrier of AS)

AS is non empty V67() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct

the carrier of AS is set

u is M2( the carrier of AS)

u1 is M2( the carrier of AS)

CESpace (AS,u,u1) is non empty strict AffinStruct

u2 is non empty () AffinStruct

AS is non empty V67() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct

the carrier of AS is set

u is M2( the carrier of AS)

u1 is M2( the carrier of AS)

CMSpace (AS,u,u1) is non empty strict AffinStruct

u2 is non empty () AffinStruct

CORTM (AS,u,u1) is M2(K24(K25(K25( the carrier of AS, the carrier of AS),K25( the carrier of AS, the carrier of AS))))

K25( the carrier of AS, the carrier of AS) is set

K25(K25( the carrier of AS, the carrier of AS),K25( the carrier of AS, the carrier of AS)) is set

K24(K25(K25( the carrier of AS, the carrier of AS),K25( the carrier of AS, the carrier of AS))) is set

AffinStruct(# the carrier of AS,(CORTM (AS,u,u1)) #) is strict AffinStruct

the carrier of u2 is set

v is M2( the carrier of u2)

v1 is M2( the carrier of u2)

w is M2( the carrier of u2)

w1 is M2( the carrier of u2)

w1 is M2( the carrier of u2)

w1 is M2( the carrier of u2)

v2 is M2( the carrier of u2)

w is M2( the carrier of u2)

u9 is M2( the carrier of AS)

u19 is M2( the carrier of AS)

v9 is M2( the carrier of AS)

v19 is M2( the carrier of AS)

w9 is M2( the carrier of AS)

w19 is M2( the carrier of AS)

u29 is M2( the carrier of AS)

v29 is M2( the carrier of AS)

v is M2( the carrier of u2)

v1 is M2( the carrier of u2)

v2 is M2( the carrier of u2)

w is M2( the carrier of u2)

w1 is M2( the carrier of AS)

w1 is M2( the carrier of AS)

w is M2( the carrier of AS)

w1 is M2( the carrier of AS)

v is M2( the carrier of u2)

v1 is M2( the carrier of u2)

w is M2( the carrier of u2)

w1 is M2( the carrier of u2)

w1 is M2( the carrier of u2)

w1 is M2( the carrier of u2)

v2 is M2( the carrier of u2)

w is M2( the carrier of u2)

u9 is M2( the carrier of AS)

u19 is M2( the carrier of AS)

v9 is M2( the carrier of AS)

v19 is M2( the carrier of AS)

w9 is M2( the carrier of AS)

w19 is M2( the carrier of AS)

u29 is M2( the carrier of AS)

v29 is M2( the carrier of AS)

v is M2( the carrier of u2)

v1 is M2( the carrier of u2)

w is M2( the carrier of u2)

w1 is M2( the carrier of u2)

w1 is M2( the carrier of u2)

w1 is M2( the carrier of u2)

v2 is M2( the carrier of u2)

w is M2( the carrier of u2)

u9 is M2( the carrier of AS)

u19 is M2( the carrier of AS)

v9 is M2( the carrier of AS)

v19 is M2( the carrier of AS)

w9 is M2( the carrier of AS)

w19 is M2( the carrier of AS)

u29 is M2( the carrier of AS)

v29 is M2( the carrier of AS)

AS is non empty V67() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct

the carrier of AS is set

u is M2( the carrier of AS)

u1 is M2( the carrier of AS)

AS is non empty V67() Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct

the carrier of AS is set

u is M2( the carrier of AS)

u1 is M2( the carrier of AS)

CMSpace (AS,u,u1) is non empty strict AffinStruct

u2 is non empty () AffinStruct

AS is non empty () AffinStruct

the carrier of AS is set

u is M2( the carrier of AS)

u1 is M2( the carrier of AS)

u2 is M2( the carrier of AS)

v is M2( the carrier of AS)

v1 is M2( the carrier of AS)

v2 is M2( the carrier of AS)

w is M2( the carrier of AS)

w1 is M2( the carrier of AS)

u is M2( the carrier of AS)

u1 is M2( the carrier of AS)

v is M2( the carrier of AS)

v1 is M2( the carrier of AS)

w is M2( the carrier of AS)

w1 is M2( the carrier of AS)

u2 is M2( the carrier of AS)

v2 is M2( the carrier of AS)

AS is non empty () AffinStruct

the carrier of AS is set

u is M2( the carrier of AS)

u1 is M2( the carrier of AS)

u2 is M2( the carrier of AS)

v is M2( the carrier of AS)

v1 is M2( the carrier of AS)

v2 is M2( the carrier of AS)

w is M2( the carrier of AS)

w1 is M2( the carrier of AS)

u is M2( the carrier of AS)

u1 is M2( the carrier of AS)

v is M2( the carrier of AS)

v1 is M2( the carrier of AS)

w is M2( the carrier of AS)

w1 is M2( the carrier of AS)

u2 is M2( the carrier of AS)

v2 is M2( the carrier of AS)

AS is non empty () AffinStruct

the carrier of AS is set

the M2( the carrier of AS) is M2( the carrier of AS)

u1 is M2( the carrier of AS)

u2 is M2( the carrier of AS)

v is M2( the carrier of AS)

v1 is M2( the carrier of AS)

v2 is M2( the carrier of AS)

w is M2( the carrier of AS)

w1 is M2( the carrier of AS)

w1 is M2( the carrier of AS)

u is M2( the carrier of AS)

u1 is M2( the carrier of AS)

u2 is M2( the carrier of AS)

v is M2( the carrier of AS)

v1 is M2( the carrier of AS)

v2 is M2( the carrier of AS)

w is M2( the carrier of AS)

w1 is M2( the carrier of AS)

w is M2( the carrier of AS)

w1 is M2( the carrier of AS)

u is M2( the carrier of AS)

u1 is M2( the carrier of AS)

v1 is M2( the carrier of AS)

v2 is M2( the carrier of AS)

u2 is M2( the carrier of AS)

v is M2( the carrier of AS)

w is M2( the carrier of AS)

w1 is M2( the carrier of AS)

w1 is M2( the carrier of AS)

u9 is M2( the carrier of AS)

w is M2( the carrier of AS)

w1 is M2( the carrier of AS)

v9 is M2( the carrier of AS)

w9 is M2( the carrier of AS)

v19 is M2( the carrier of AS)

w19 is M2( the carrier of AS)

v29 is M2( the carrier of AS)

c

u19 is M2( the carrier of AS)

u29 is M2( the carrier of AS)

AS is non empty () AffinStruct

the carrier of AS is set

u is M2( the carrier of AS)

u1 is M2( the carrier of AS)

u2 is M2( the carrier of AS)

v is M2( the carrier of AS)

v1 is M2( the carrier of AS)

v2 is M2( the carrier of AS)

w is M2( the carrier of AS)

w1 is M2( the carrier of AS)

w is M2( the carrier of AS)

w1 is M2( the carrier of AS)

w1 is M2( the carrier of AS)

u9 is M2( the carrier of AS)

v9 is M2( the carrier of AS)

w9 is M2( the carrier of AS)

u19 is M2( the carrier of AS)

v19 is M2( the carrier of AS)

u is M2( the carrier of AS)

u1 is M2( the carrier of AS)

u2 is M2( the carrier of AS)

v is M2( the carrier of AS)

v1 is M2( the carrier of AS)

v2 is M2( the carrier of AS)

w is M2( the carrier of AS)

w1 is M2( the carrier of AS)