:: ALTCAT_3 semantic presentation

K132() is set

bool K132() is set

{} is empty trivial Function-like functional set

dom {} is set

rng {} is set

C is non empty with_units AltCatStr

the U1 of C is set

o1 is Element of the U1 of C

o2 is Element of the U1 of C

<^o1,o2^> is set

<^o2,o1^> is set

C is non empty with_units AltCatStr

the U1 of C is set

o1 is Element of the U1 of C

o2 is Element of the U1 of C

<^o1,o2^> is set

<^o2,o1^> is set

C is non empty with_units AltCatStr

the U1 of C is set

o1 is Element of the U1 of C

o2 is Element of the U1 of C

<^o1,o2^> is set

C is non empty with_units AltCatStr

the U1 of C is set

o1 is Element of the U1 of C

o2 is Element of the U1 of C

<^o1,o2^> is set

C is non empty with_units AltCatStr

the U1 of C is set

o1 is Element of the U1 of C

idm o1 is Element of <^o1,o1^>

<^o1,o1^> is set

(idm o1) * (idm o1) is Element of <^o1,o1^>

C is non empty transitive associative with_units AltCatStr

the U1 of C is set

o1 is Element of the U1 of C

o2 is Element of the U1 of C

<^o1,o2^> is set

<^o2,o1^> is set

o3 is Element of <^o1,o2^>

M1 is Element of <^o2,o1^>

M2 is Element of <^o2,o1^>

idm o1 is Element of <^o1,o1^>

<^o1,o1^> is set

(idm o1) * M1 is Element of <^o2,o1^>

M2 * o3 is Element of <^o1,o1^>

(M2 * o3) * M1 is Element of <^o2,o1^>

o3 * M1 is Element of <^o2,o2^>

<^o2,o2^> is set

M2 * (o3 * M1) is Element of <^o2,o1^>

idm o2 is Element of <^o2,o2^>

M2 * (idm o2) is Element of <^o2,o1^>

M1 is Element of <^o2,o1^>

M2 is Element of <^o2,o1^>

idm o2 is Element of <^o2,o2^>

<^o2,o2^> is set

M1 * (idm o2) is Element of <^o2,o1^>

o3 * M2 is Element of <^o2,o2^>

M1 * (o3 * M2) is Element of <^o2,o1^>

M1 * o3 is Element of <^o1,o1^>

<^o1,o1^> is set

(M1 * o3) * M2 is Element of <^o2,o1^>

idm o1 is Element of <^o1,o1^>

(idm o1) * M2 is Element of <^o2,o1^>

C is non empty transitive associative with_units AltCatStr

the U1 of C is set

o1 is Element of the U1 of C

o2 is Element of the U1 of C

<^o1,o2^> is set

<^o2,o1^> is set

idm o1 is Element of <^o1,o1^>

<^o1,o1^> is set

idm o2 is Element of <^o2,o2^>

<^o2,o2^> is set

o3 is Element of <^o1,o2^>

(C,o1,o2,o3) is Element of <^o2,o1^>

(C,o1,o2,o3) * o3 is Element of <^o1,o1^>

o3 * (C,o1,o2,o3) is Element of <^o2,o2^>

C is non empty transitive associative with_units AltCatStr

the U1 of C is set

o1 is Element of the U1 of C

o2 is Element of the U1 of C

<^o1,o2^> is set

<^o2,o1^> is set

o3 is Element of <^o1,o2^>

(C,o1,o2,o3) is Element of <^o2,o1^>

(C,o2,o1,(C,o1,o2,o3)) is Element of <^o1,o2^>

idm o2 is Element of <^o2,o2^>

<^o2,o2^> is set

(idm o2) * (C,o2,o1,(C,o1,o2,o3)) is Element of <^o1,o2^>

o3 * (C,o1,o2,o3) is Element of <^o2,o2^>

(o3 * (C,o1,o2,o3)) * (C,o2,o1,(C,o1,o2,o3)) is Element of <^o1,o2^>

(C,o1,o2,o3) * (C,o2,o1,(C,o1,o2,o3)) is Element of <^o1,o1^>

<^o1,o1^> is set

o3 * ((C,o1,o2,o3) * (C,o2,o1,(C,o1,o2,o3))) is Element of <^o1,o2^>

idm o1 is Element of <^o1,o1^>

o3 * (idm o1) is Element of <^o1,o2^>

C is non empty transitive associative with_units AltCatStr

the U1 of C is set

o1 is Element of the U1 of C

idm o1 is Element of <^o1,o1^>

<^o1,o1^> is set

(C,o1,o1,(idm o1)) is Element of <^o1,o1^>

(C,o1,o1,(idm o1)) * (idm o1) is Element of <^o1,o1^>

C is non empty transitive associative with_units AltCatStr

the U1 of C is set

o1 is Element of the U1 of C

o2 is Element of the U1 of C

<^o1,o2^> is set

C is non empty transitive associative with_units AltCatStr

the U1 of C is set

o1 is Element of the U1 of C

o2 is Element of the U1 of C

<^o1,o2^> is set

o3 is Element of <^o1,o2^>

(C,o1,o2,o3) is Element of <^o2,o1^>

<^o2,o1^> is set

o3 * (C,o1,o2,o3) is Element of <^o2,o2^>

<^o2,o2^> is set

idm o2 is Element of <^o2,o2^>

(C,o1,o2,o3) * o3 is Element of <^o1,o1^>

<^o1,o1^> is set

idm o1 is Element of <^o1,o1^>

C is non empty transitive associative with_units AltCatStr

the U1 of C is set

o1 is Element of the U1 of C

o2 is Element of the U1 of C

<^o1,o2^> is set

<^o2,o1^> is set

o3 is Element of <^o1,o2^>

(C,o1,o2,o3) is Element of <^o2,o1^>

o3 * (C,o1,o2,o3) is Element of <^o2,o2^>

<^o2,o2^> is set

idm o2 is Element of <^o2,o2^>

(C,o1,o2,o3) * o3 is Element of <^o1,o1^>

<^o1,o1^> is set

idm o1 is Element of <^o1,o1^>

C is non empty transitive associative with_units AltCatStr

the U1 of C is set

o1 is Element of the U1 of C

o2 is Element of the U1 of C

<^o1,o2^> is set

o3 is Element of the U1 of C

<^o2,o3^> is set

<^o3,o1^> is set

M1 is Element of <^o1,o2^>

(C,o1,o2,M1) is Element of <^o2,o1^>

<^o2,o1^> is set

M2 is Element of <^o2,o3^>

M2 * M1 is Element of <^o1,o3^>

<^o1,o3^> is set

(C,o1,o3,(M2 * M1)) is Element of <^o3,o1^>

(C,o2,o3,M2) is Element of <^o3,o2^>

<^o3,o2^> is set

(C,o1,o2,M1) * (C,o2,o3,M2) is Element of <^o3,o1^>

o is Element of <^o2,o1^>

B1 is Element of <^o3,o2^>

o * B1 is Element of <^o3,o1^>

(M2 * M1) * (o * B1) is Element of <^o3,o3^>

<^o3,o3^> is set

M1 * (o * B1) is Element of <^o3,o2^>

M2 * (M1 * (o * B1)) is Element of <^o3,o3^>

M1 * o is Element of <^o2,o2^>

<^o2,o2^> is set

(M1 * o) * B1 is Element of <^o3,o2^>

M2 * ((M1 * o) * B1) is Element of <^o3,o3^>

idm o2 is Element of <^o2,o2^>

(idm o2) * B1 is Element of <^o3,o2^>

M2 * ((idm o2) * B1) is Element of <^o3,o3^>

M2 * B1 is Element of <^o3,o3^>

idm o3 is Element of <^o3,o3^>

(o * B1) * (M2 * M1) is Element of <^o1,o1^>

<^o1,o1^> is set

B1 * (M2 * M1) is Element of <^o1,o2^>

o * (B1 * (M2 * M1)) is Element of <^o1,o1^>

B1 * M2 is Element of <^o2,o2^>

(B1 * M2) * M1 is Element of <^o1,o2^>

o * ((B1 * M2) * M1) is Element of <^o1,o1^>

(idm o2) * M1 is Element of <^o1,o2^>

o * ((idm o2) * M1) is Element of <^o1,o1^>

o * M1 is Element of <^o1,o1^>

idm o1 is Element of <^o1,o1^>

C is non empty transitive associative with_units AltCatStr

the U1 of C is set

o3 is Element of the U1 of C

<^o3,o3^> is set

idm o3 is Element of <^o3,o3^>

(C,o3,o3,(idm o3)) is Element of <^o3,o3^>

(C,o3,o3,(idm o3)) * (idm o3) is Element of <^o3,o3^>

(idm o3) * (idm o3) is Element of <^o3,o3^>

(idm o3) * (C,o3,o3,(idm o3)) is Element of <^o3,o3^>

o3 is Element of the U1 of C

M1 is Element of the U1 of C

<^o3,M1^> is set

<^M1,o3^> is set

M2 is Element of <^o3,M1^>

M2 is Element of <^o3,M1^>

(C,o3,M1,M2) is Element of <^M1,o3^>

o is Element of <^M1,o3^>

(C,M1,o3,o) is Element of <^o3,M1^>

(C,M1,o3,o) * o is Element of <^M1,M1^>

<^M1,M1^> is set

M2 * (C,o3,M1,M2) is Element of <^M1,M1^>

idm M1 is Element of <^M1,M1^>

o * (C,M1,o3,o) is Element of <^o3,o3^>

<^o3,o3^> is set

(C,o3,M1,M2) * M2 is Element of <^o3,o3^>

idm o3 is Element of <^o3,o3^>

C is non empty transitive associative with_units AltCatStr

the U1 of C is set

o1 is Element of the U1 of C

o2 is Element of the U1 of C

o3 is Element of the U1 of C

<^o1,o2^> is set

<^o2,o3^> is set

M1 is Element of <^o2,o3^>

M2 is Element of <^o1,o2^>

<^o2,o1^> is set

<^o3,o2^> is set

<^o1,o3^> is set

<^o3,o1^> is set

M1 * M2 is Element of <^o1,o3^>

C is non empty AltCatStr

the U1 of C is set

o1 is Element of the U1 of C

o2 is Element of the U1 of C

<^o1,o2^> is set

C is non empty AltCatStr

the U1 of C is set

o1 is Element of the U1 of C

o2 is Element of the U1 of C

<^o1,o2^> is set

C is non empty transitive associative AltCatStr

the U1 of C is set

o1 is Element of the U1 of C

o2 is Element of the U1 of C

<^o1,o2^> is set

o3 is Element of the U1 of C

<^o2,o3^> is set

M1 is Element of <^o1,o2^>

M2 is Element of <^o2,o3^>

M2 * M1 is Element of <^o1,o3^>

<^o1,o3^> is set

o is Element of the U1 of C

<^o,o1^> is set

<^o,o2^> is set

B1 is Element of <^o,o1^>

(M2 * M1) * B1 is Element of <^o,o3^>

<^o,o3^> is set

A is Element of <^o,o1^>

(M2 * M1) * A is Element of <^o,o3^>

M1 * B1 is Element of <^o,o2^>

M2 * (M1 * B1) is Element of <^o,o3^>

M1 * A is Element of <^o,o2^>

M2 * (M1 * A) is Element of <^o,o3^>

C is non empty transitive associative AltCatStr

the U1 of C is set

o1 is Element of the U1 of C

o2 is Element of the U1 of C

<^o1,o2^> is set

o3 is Element of the U1 of C

<^o2,o3^> is set

M1 is Element of <^o1,o2^>

M2 is Element of <^o2,o3^>

M2 * M1 is Element of <^o1,o3^>

<^o1,o3^> is set

o is Element of the U1 of C

<^o3,o^> is set

<^o2,o^> is set

B1 is Element of <^o3,o^>

B1 * (M2 * M1) is Element of <^o1,o^>

<^o1,o^> is set

A is Element of <^o3,o^>

A * (M2 * M1) is Element of <^o1,o^>

B1 * M2 is Element of <^o2,o^>

(B1 * M2) * M1 is Element of <^o1,o^>

A * M2 is Element of <^o2,o^>

(A * M2) * M1 is Element of <^o1,o^>

C is non empty transitive associative AltCatStr

the U1 of C is set

o1 is Element of the U1 of C

o2 is Element of the U1 of C

<^o1,o2^> is set

o3 is Element of the U1 of C

<^o2,o3^> is set

M1 is Element of <^o1,o2^>

M2 is Element of <^o2,o3^>

M2 * M1 is Element of <^o1,o3^>

<^o1,o3^> is set

o is Element of the U1 of C

<^o,o1^> is set

B1 is Element of <^o,o1^>

M1 * B1 is Element of <^o,o2^>

<^o,o2^> is set

A is Element of <^o,o1^>

M1 * A is Element of <^o,o2^>

(M2 * M1) * B1 is Element of <^o,o3^>

<^o,o3^> is set

M2 * (M1 * B1) is Element of <^o,o3^>

(M2 * M1) * A is Element of <^o,o3^>

M2 * (M1 * A) is Element of <^o,o3^>

C is non empty transitive associative AltCatStr

the U1 of C is set

o1 is Element of the U1 of C

o2 is Element of the U1 of C

<^o1,o2^> is set

o3 is Element of the U1 of C

<^o2,o3^> is set

M1 is Element of <^o1,o2^>

M2 is Element of <^o2,o3^>

M2 * M1 is Element of <^o1,o3^>

<^o1,o3^> is set

o is Element of the U1 of C

<^o3,o^> is set

B1 is Element of <^o3,o^>

B1 * M2 is Element of <^o2,o^>

<^o2,o^> is set

A is Element of <^o3,o^>

A * M2 is Element of <^o2,o^>

(B1 * M2) * M1 is Element of <^o1,o^>

<^o1,o^> is set

B1 * (M2 * M1) is Element of <^o1,o^>

(A * M2) * M1 is Element of <^o1,o^>

A * (M2 * M1) is Element of <^o1,o^>

C is non empty with_units AltCatStr

the U1 of C is set

o1 is Element of the U1 of C

idm o1 is Element of <^o1,o1^>

<^o1,o1^> is set

o2 is Element of the U1 of C

<^o1,o2^> is set

o3 is Element of <^o1,o2^>

o3 * (idm o1) is Element of <^o1,o2^>

M1 is Element of <^o1,o2^>

M1 * (idm o1) is Element of <^o1,o2^>

o2 is Element of the U1 of C

<^o2,o1^> is set

o3 is Element of <^o2,o1^>

(idm o1) * o3 is Element of <^o2,o1^>

M1 is Element of <^o2,o1^>

(idm o1) * M1 is Element of <^o2,o1^>

C is non empty set

EnsCat C is non empty transitive strict quasi-functional semi-functional pseudo-functional associative with_units AltCatStr

the U1 of (EnsCat C) is set

o1 is Element of the U1 of (EnsCat C)

o2 is Element of the U1 of (EnsCat C)

<^o1,o2^> is set

[:o1,o2:] is set

bool [:o1,o2:] is set

o3 is Element of <^o1,o2^>

M1 is Relation-like o1 -defined o2 -valued Function-like quasi_total Element of bool [:o1,o2:]

dom M1 is set

o is set

B1 is set

M1 . o is set

M1 . B1 is set

o1 --> B1 is Relation-like o1 -defined {B1} -valued Function-like quasi_total Element of bool [:o1,{B1}:]

{B1} is non empty trivial set

[:o1,{B1}:] is set

bool [:o1,{B1}:] is set

o1 --> o is Relation-like o1 -defined {o} -valued Function-like quasi_total Element of bool [:o1,{o}:]

{o} is non empty trivial set

[:o1,{o}:] is set

bool [:o1,{o}:] is set

dom (o1 --> B1) is set

rng (o1 --> B1) is set

B2 is set

y is set

(o1 --> B1) . y is set

(o1 --> B1) * M1 is Relation-like Function-like set

dom ((o1 --> B1) * M1) is set

Funcs (o1,o1) is set

<^o1,o1^> is set

the Element of o1 is Element of o1

(o1 --> o) . the Element of o1 is set

(o1 --> B1) . the Element of o1 is set

dom (o1 --> o) is set

rng (o1 --> o) is set

A1 is set

x is set

(o1 --> o) . x is set

(o1 --> o) * M1 is Relation-like Function-like set

dom ((o1 --> o) * M1) is set

x is set

((o1 --> o) * M1) . x is set

(o1 --> o) . x is set

M1 . ((o1 --> o) . x) is set

(o1 --> B1) . x is set

M1 . ((o1 --> B1) . x) is set

((o1 --> B1) * M1) . x is set

A1 is Element of <^o1,o1^>

o3 * A1 is Element of <^o1,o2^>

B2 is Element of <^o1,o1^>

o3 * B2 is Element of <^o1,o2^>

M2 is Element of the U1 of (EnsCat C)

<^M2,o1^> is set

<^M2,o2^> is set

o is Element of <^M2,o1^>

o3 * o is Element of <^M2,o2^>

B1 is Element of <^M2,o1^>

o3 * B1 is Element of <^M2,o2^>

Funcs (M2,o1) is set

A is Relation-like Function-like set

dom A is set

rng A is set

B is Relation-like Function-like set

dom B is set

rng B is set

A * M1 is Relation-like Function-like set

B * M1 is Relation-like Function-like set

B2 is set

A . B2 is set

M1 . (A . B2) is set

(A * M1) . B2 is set

B . B2 is set

M1 . (B . B2) is set

Funcs (o1,o2) is set

the Element of Funcs (o1,o2) is Element of Funcs (o1,o2)

o is Element of the U1 of (EnsCat C)

<^o,o1^> is set

B1 is Relation-like Function-like set

dom B1 is set

rng B1 is set

A is Element of <^o,o1^>

o3 * A is Element of <^o,o2^>

<^o,o2^> is set

B is Element of <^o,o1^>

o3 * B is Element of <^o,o2^>

Funcs (o,o1) is set

B2 is Relation-like Function-like set

dom B2 is set

rng B2 is set

y is Relation-like Function-like set

dom y is set

rng y is set

C is non empty with_non-empty_elements non empty-membered set

EnsCat C is non empty transitive strict quasi-functional semi-functional pseudo-functional associative with_units AltCatStr

the U1 of (EnsCat C) is set

o1 is Element of the U1 of (EnsCat C)

o2 is Element of the U1 of (EnsCat C)

<^o1,o2^> is set

[:o1,o2:] is set

bool [:o1,o2:] is set

o3 is Element of <^o1,o2^>

M1 is Relation-like o1 -defined o2 -valued Function-like quasi_total Element of bool [:o1,o2:]

M2 is set

{M2} is non empty trivial set

dom M1 is set

rng M1 is set

o is set

{o} is non empty trivial set

M2 is Element of the U1 of (EnsCat C)

<^o2,M2^> is set

<^o1,M2^> is set

o is Element of <^o2,M2^>

o * o3 is Element of <^o1,M2^>

B1 is Element of <^o2,M2^>

B1 * o3 is Element of <^o1,M2^>

Funcs (o2,M2) is set

A is Relation-like Function-like set

dom A is set

rng A is set

B is Relation-like Function-like set

dom B is set

rng B is set

M1 * A is Relation-like Function-like set

M1 * B is Relation-like Function-like set

B2 is set

A . B2 is set

B . B2 is set

rng M1 is set

dom M1 is set

y is set

M1 . y is set

A . (M1 . y) is set

(M1 * A) . y is set

M2 is set

M2 is set

dom M1 is set

o is Element of the U1 of (EnsCat C)

the Element of o is Element of o

rng M1 is set

{ the Element of o} is non empty trivial set

o \ { the Element of o} is Element of bool o

bool o is set

B is set

o2 --> the Element of o is Relation-like o2 -defined { the Element of o} -valued Function-like quasi_total Element of bool [:o2,{ the Element of o}:]

[:o2,{ the Element of o}:] is set

bool [:o2,{ the Element of o}:] is set

dom (o2 --> the Element of o) is set

rng (o2 --> the Element of o) is set

y is set

A1 is set

(o2 --> the Element of o) . A1 is set

Funcs (o2,o) is set

<^o2,o^> is set

A is non empty set

the Element of A is Element of A

x is Element of o

z is Relation-like Function-like set

dom z is set

M1 * z is Relation-like Function-like set

dom (M1 * z) is set

rng z is set

A2 is set

z is set

z . z is set

IFEQ (z,B,x, the Element of o) is Element of o

IFEQ (z,B,x, the Element of o) is Element of o

rng (M1 * z) is set

z is set

Funcs (o1,o) is set

<^o1,o^> is set

z . B is set

IFEQ (B,B,x, the Element of o) is Element of o

M1 * (o2 --> the Element of o) is Relation-like Function-like set

dom (M1 * (o2 --> the Element of o)) is set

z is set

M1 . z is set

z . (M1 . z) is set

IFEQ ((M1 . z),B,x, the Element of o) is Element of o

(M1 * z) . z is set

(o2 --> the Element of o) . (M1 . z) is set

(M1 * (o2 --> the Element of o)) . z is set

A2 is Element of <^o2,o^>

A2 * o3 is Element of <^o1,o^>

y is Element of <^o2,o^>

y * o3 is Element of <^o1,o^>

B1 is Element of the U1 of (EnsCat C)

<^o2,B1^> is set

<^o1,B1^> is set

A is Element of <^o2,B1^>

A * o3 is Element of <^o1,B1^>

B is Element of <^o2,B1^>

B * o3 is Element of <^o1,B1^>

Funcs (o2,B1) is set

B2 is Relation-like Function-like set

dom B2 is set

rng B2 is set

y is Relation-like Function-like set

dom y is set

rng y is set

M1 * B2 is Relation-like Function-like set

M1 * y is Relation-like Function-like set

A1 is set

B2 . A1 is set

y . A1 is set

rng M1 is set

x is set

M1 . x is set

B2 . (M1 . x) is set

(M1 * B2) . x is set

M2 is Element of the U1 of (EnsCat C)

<^o2,M2^> is set

o is Element of <^o2,M2^>

o * o3 is Element of <^o1,M2^>

<^o1,M2^> is set

B1 is Element of <^o2,M2^>

B1 * o3 is Element of <^o1,M2^>

Funcs (o2,M2) is set

A is Relation-like Function-like set

dom A is set

rng A is set

B is Relation-like Function-like set

dom B is set

rng B is set

M2 is set

C is non empty transitive associative with_units AltCatStr

the U1 of C is set

o1 is Element of the U1 of C

o2 is Element of the U1 of C

<^o1,o2^> is set

<^o2,o1^> is set

o3 is Element of <^o1,o2^>

M1 is Element of <^o2,o1^>

M2 is Element of the U1 of C

<^o2,M2^> is set

o is Element of <^o2,M2^>

o * o3 is Element of <^o1,M2^>

<^o1,M2^> is set

B1 is Element of <^o2,M2^>

B1 * o3 is Element of <^o1,M2^>

idm o2 is Element of <^o2,o2^>

<^o2,o2^> is set

o * (idm o2) is Element of <^o2,M2^>

o3 * M1 is Element of <^o2,o2^>

o * (o3 * M1) is Element of <^o2,M2^>

(B1 * o3) * M1 is Element of <^o2,M2^>

B1 * (o3 * M1) is Element of <^o2,M2^>

B1 * (idm o2) is Element of <^o2,M2^>

C is non empty transitive associative with_units AltCatStr

the U1 of C is set

o1 is Element of the U1 of C

o2 is Element of the U1 of C

<^o1,o2^> is set

<^o2,o1^> is set

o3 is Element of <^o1,o2^>

M1 is Element of <^o2,o1^>

M2 is Element of the U1 of C

<^M2,o1^> is set

o is Element of <^M2,o1^>

o3 * o is Element of <^M2,o2^>

<^M2,o2^> is set

B1 is Element of <^M2,o1^>

o3 * B1 is Element of <^M2,o2^>

idm o1 is Element of <^o1,o1^>

<^o1,o1^> is set

(idm o1) * o is Element of <^M2,o1^>

M1 * o3 is Element of <^o1,o1^>

(M1 * o3) * o is Element of <^M2,o1^>

M1 * (o3 * B1) is Element of <^M2,o1^>

(M1 * o3) * B1 is Element of <^M2,o1^>

(idm o1) * B1 is Element of <^M2,o1^>

C is non empty transitive associative with_units AltCatStr

the U1 of C is set

o1 is Element of the U1 of C

o2 is Element of the U1 of C

<^o1,o2^> is set

<^o2,o1^> is set

o3 is Element of <^o1,o2^>

M1 is Element of the U1 of C

<^o2,M1^> is set

M2 is Element of <^o2,M1^>

M2 * o3 is Element of <^o1,M1^>

<^o1,M1^> is set

o is Element of <^o2,M1^>

o * o3 is Element of <^o1,M1^>

(C,o1,o2,o3) is Element of <^o2,o1^>

o3 * (C,o1,o2,o3) is Element of <^o2,o2^>

<^o2,o2^> is set

M2 * (o3 * (C,o1,o2,o3)) is Element of <^o2,M1^>

(o * o3) * (C,o1,o2,o3) is Element of <^o2,M1^>

idm o2 is Element of <^o2,o2^>

M2 * (idm o2) is Element of <^o2,M1^>

o * (o3 * (C,o1,o2,o3)) is Element of <^o2,M1^>

o * (idm o2) is Element of <^o2,M1^>

M1 is Element of the U1 of C

<^M1,o1^> is set

M2 is Element of <^M1,o1^>

o3 * M2 is Element of <^M1,o2^>

<^M1,o2^> is set

o is Element of <^M1,o1^>

o3 * o is Element of <^M1,o2^>

(C,o1,o2,o3) is Element of <^o2,o1^>

(C,o1,o2,o3) * o3 is Element of <^o1,o1^>

<^o1,o1^> is set

((C,o1,o2,o3) * o3) * M2 is Element of <^M1,o1^>

(C,o1,o2,o3) * (o3 * o) is Element of <^M1,o1^>

idm o1 is Element of <^o1,o1^>

(idm o1) * M2 is Element of <^M1,o1^>

((C,o1,o2,o3) * o3) * o is Element of <^M1,o1^>

(idm o1) * o is Element of <^M1,o1^>

C is non empty transitive associative with_units AltCatStr

the U1 of C is set

o1 is Element of the U1 of C

o2 is Element of the U1 of C

<^o1,o2^> is set

o3 is Element of the U1 of C

<^o2,o3^> is set

<^o3,o1^> is set

<^o2,o1^> is set

<^o3,o2^> is set

M1 is Element of <^o1,o2^>

M2 is Element of <^o2,o3^>

M2 * M1 is Element of <^o1,o3^>

<^o1,o3^> is set

o is Element of <^o2,o1^>

B1 is Element of <^o3,o2^>

o * B1 is Element of <^o3,o1^>

A is Element of <^o3,o1^>

(M2 * M1) * A is Element of <^o3,o3^>

<^o3,o3^> is set

M1 * (o * B1) is Element of <^o3,o2^>

M2 * (M1 * (o * B1)) is Element of <^o3,o3^>

M1 * o is Element of <^o2,o2^>

<^o2,o2^> is set

(M1 * o) * B1 is Element of <^o3,o2^>

M2 * ((M1 * o) * B1) is Element of <^o3,o3^>

idm o2 is Element of <^o2,o2^>

(idm o2) * B1 is Element of <^o3,o2^>

M2 * ((idm o2) * B1) is Element of <^o3,o3^>

M2 * B1 is Element of <^o3,o3^>

idm o3 is Element of <^o3,o3^>

C is non empty transitive associative with_units AltCatStr

the U1 of C is set

o1 is Element of the U1 of C

o2 is Element of the U1 of C

<^o1,o2^> is set

o3 is Element of the U1 of C

<^o2,o3^> is set

<^o3,o1^> is set

<^o2,o1^> is set

<^o3,o2^> is set

M1 is Element of <^o1,o2^>

M2 is Element of <^o2,o3^>

M2 * M1 is Element of <^o1,o3^>

<^o1,o3^> is set

o is Element of <^o2,o1^>

B1 is Element of <^o3,o2^>

o * B1 is Element of <^o3,o1^>

A is Element of <^o3,o1^>

<^o2,o2^> is set

A * (M2 * M1) is Element of <^o1,o1^>

<^o1,o1^> is set

(o * B1) * M2 is Element of <^o2,o1^>

((o * B1) * M2) * M1 is Element of <^o1,o1^>

B1 * M2 is Element of <^o2,o2^>

o * (B1 * M2) is Element of <^o2,o1^>

(o * (B1 * M2)) * M1 is Element of <^o1,o1^>

idm o2 is Element of <^o2,o2^>

o * (idm o2) is Element of <^o2,o1^>

(o * (idm o2)) * M1 is Element of <^o1,o1^>

(idm o2) * M1 is Element of <^o1,o2^>

o * ((idm o2) * M1) is Element of <^o1,o1^>

o * M1 is Element of <^o1,o1^>

idm o1 is Element of <^o1,o1^>

C is non empty transitive associative with_units AltCatStr

the U1 of C is set

o1 is Element of the U1 of C

o2 is Element of the U1 of C

<^o1,o2^> is set

<^o2,o1^> is set

o3 is Element of <^o1,o2^>

M1 is Element of <^o2,o1^>

o3 * M1 is Element of <^o2,o2^>

<^o2,o2^> is set

(o3 * M1) * o3 is Element of <^o1,o2^>

idm o2 is Element of <^o2,o2^>

(idm o2) * o3 is Element of <^o1,o2^>

M1 * o3 is Element of <^o1,o1^>

<^o1,o1^> is set

o3 * (M1 * o3) is Element of <^o1,o2^>

idm o1 is Element of <^o1,o1^>

o3 * (idm o1) is Element of <^o1,o2^>

(C,o1,o2,o3) is Element of <^o2,o1^>

o3 * (C,o1,o2,o3) is Element of <^o2,o2^>

(C,o1,o2,o3) * o3 is Element of <^o1,o1^>

C is non empty transitive associative with_units AltCatStr

the U1 of C is set

o1 is Element of the U1 of C

o2 is Element of the U1 of C

<^o1,o2^> is set

<^o2,o1^> is set

o3 is Element of <^o1,o2^>

M1 is Element of <^o2,o1^>

M1 * o3 is Element of <^o1,o1^>

<^o1,o1^> is set

o3 * (M1 * o3) is Element of <^o1,o2^>

idm o1 is Element of <^o1,o1^>

o3 * (idm o1) is Element of <^o1,o2^>

idm o2 is Element of <^o2,o2^>

<^o2,o2^> is set

(idm o2) * o3 is Element of <^o1,o2^>

o3 * M1 is Element of <^o2,o2^>

(o3 * M1) * o3 is Element of <^o1,o2^>

(C,o1,o2,o3) is Element of <^o2,o1^>

(C,o1,o2,o3) * o3 is Element of <^o1,o1^>

o3 * (C,o1,o2,o3) is Element of <^o2,o2^>

C is non empty transitive associative with_units AltCatStr

the U1 of C is set

o1 is Element of the U1 of C

o2 is Element of the U1 of C

<^o1,o2^> is set

o3 is Element of the U1 of C

<^o2,o3^> is set

<^o3,o1^> is set

M1 is Element of <^o1,o2^>

M2 is Element of <^o2,o3^>

M2 * M1 is Element of <^o1,o3^>

<^o1,o3^> is set

o is Element of <^o3,o1^>

(M2 * M1) * o is Element of <^o3,o3^>

<^o3,o3^> is set

idm o3 is Element of <^o3,o3^>

M1 * o is Element of <^o3,o2^>

<^o3,o2^> is set

M2 * (M1 * o) is Element of <^o3,o3^>

C is non empty transitive associative with_units AltCatStr

the U1 of C is set

o1 is Element of the U1 of C

o2 is Element of the U1 of C

<^o1,o2^> is set

o3 is Element of the U1 of C

<^o2,o3^> is set

<^o3,o1^> is set

M1 is Element of <^o1,o2^>

M2 is Element of <^o2,o3^>

M2 * M1 is Element of <^o1,o3^>

<^o1,o3^> is set

o is Element of <^o3,o1^>

o * M2 is Element of <^o2,o1^>

<^o2,o1^> is set

(o * M2) * M1 is Element of <^o1,o1^>

<^o1,o1^> is set

o * (M2 * M1) is Element of <^o1,o1^>

idm o1 is Element of <^o1,o1^>

C is non empty transitive associative with_units AltCatStr

the U1 of C is set

o1 is Element of the U1 of C

o2 is Element of the U1 of C

<^o1,o2^> is set

<^o2,o1^> is set

o3 is Element of <^o1,o2^>

M1 is Element of <^o2,o1^>

o3 * M1 is Element of <^o2,o2^>

<^o2,o2^> is set

M1 * (o3 * M1) is Element of <^o2,o1^>

idm o2 is Element of <^o2,o2^>

M1 * (idm o2) is Element of <^o2,o1^>

M1 * o3 is Element of <^o1,o1^>

<^o1,o1^> is set

(M1 * o3) * M1 is Element of <^o2,o1^>

idm o1 is Element of <^o1,o1^>

(idm o1) * M1 is Element of <^o2,o1^>

C is non empty with_units AltCatStr

the U1 of C is set

o1 is Element of the U1 of C

<^o1,o1^> is set

idm o1 is Element of <^o1,o1^>

C is non empty transitive associative with_units AltCatStr

the U1 of C is set

o1 is Element of the U1 of C

<^o1,o1^> is set

idm o1 is Element of <^o1,o1^>

o2 is Element of <^o1,o1^>

C is non empty transitive associative with_units AltCatStr

the U1 of C is set

o1 is Element of the U1 of C

<^o1,o1^> is set

o3 is (C,o1,o1) Element of <^o1,o1^>

o2 is (C,o1,o1) Element of <^o1,o1^>

o2 * o3 is Element of <^o1,o1^>

C is non empty transitive associative with_units AltCatStr

the U1 of C is set

o1 is Element of the U1 of C

<^o1,o1^> is set

o3 is (C,o1,o1) Element of <^o1,o1^>

o2 is (C,o1,o1) Element of <^o1,o1^>

o2 * o3 is Element of <^o1,o1^>

C is non empty transitive associative with_units AltCatStr

the U1 of C is set

o1 is Element of the U1 of C

<^o1,o1^> is set

o3 is (C,o1,o1) Element of <^o1,o1^>

o2 is (C,o1,o1) Element of <^o1,o1^>

o2 * o3 is Element of <^o1,o1^>

C is non empty transitive associative with_units AltCatStr

the U1 of C is set

o1 is Element of the U1 of C

<^o1,o1^> is set

o3 is (C,o1,o1) Element of <^o1,o1^>

o2 is (C,o1,o1) Element of <^o1,o1^>

o2 * o3 is Element of <^o1,o1^>

C is non empty transitive associative with_units AltCatStr

the U1 of C is set

o1 is Element of the U1 of C

<^o1,o1^> is set

o3 is (C,o1,o1) Element of <^o1,o1^>

o2 is (C,o1,o1) Element of <^o1,o1^>

o2 * o3 is Element of <^o1,o1^>

C is AltGraph

the U1 of C is set

C is AltGraph

the U1 of C is set

o1 is Element of the U1 of C

o2 is Element of the U1 of C

<^o1,o2^> is set

o3 is Element of <^o1,o2^>

{o3} is non empty trivial set

M1 is set

{M1} is non empty trivial set

M1 is Element of <^o1,o2^>

o2 is Element of the U1 of C

<^o1,o2^> is set

o3 is Element of <^o1,o2^>

{o3} is non empty trivial set

M1 is set

M2 is Element of <^o1,o2^>

M1 is set

C is non empty transitive associative with_units AltCatStr

the U1 of C is set

o1 is Element of the U1 of C

o2 is Element of the U1 of C

<^o2,o2^> is set

o3 is Element of <^o2,o2^>

o3 is set

{o3} is non empty trivial set

<^o2,o1^> is set

M1 is Element of <^o2,o1^>

<^o1,o2^> is set

M2 is Element of <^o1,o2^>

M2 * M1 is Element of <^o2,o2^>

idm o2 is Element of <^o2,o2^>

<^o1,o1^> is set

o is Element of <^o1,o1^>

o is set

{o} is non empty trivial set

M1 * M2 is Element of <^o1,o1^>

idm o1 is Element of <^o1,o1^>

C is AltGraph

the U1 of C is set

C is AltGraph

the U1 of C is set

o1 is Element of the U1 of C

o2 is Element of the U1 of C

<^o2,o1^> is set

o3 is Element of <^o2,o1^>

{o3} is non empty trivial set

M1 is set

{M1} is non empty trivial set

M1 is Element of <^o2,o1^>

o2 is Element of the U1 of C

<^o2,o1^> is set

o3 is Element of <^o2,o1^>

{o3} is non empty trivial set

M1 is set

M2 is Element of <^o2,o1^>

M1 is set

C is non empty transitive associative with_units AltCatStr

the U1 of C is set

o1 is Element of the U1 of C

o2 is Element of the U1 of C

<^o1,o1^> is set

o3 is Element of <^o1,o1^>

o3 is set

{o3} is non empty trivial set

<^o2,o1^> is set

M1 is Element of <^o2,o1^>

<^o1,o2^> is set

M2 is Element of <^o1,o2^>

M1 * M2 is Element of <^o1,o1^>

idm o1 is Element of <^o1,o1^>

<^o2,o2^> is set

o is Element of <^o2,o2^>

o is set

{o} is non empty trivial set

M2 * M1 is Element of <^o2,o2^>

idm o2 is Element of <^o2,o2^>

C is AltGraph

the U1 of C is set

C is non empty transitive associative with_units AltCatStr

the U1 of C is set

o1 is Element of the U1 of C

o2 is Element of the U1 of C

C is non empty AltCatStr

the U1 of C is set

o1 is Element of the U1 of C

o2 is Element of the U1 of C

<^o1,o2^> is set

C is non empty transitive associative with_units AltCatStr

the U1 of C is set

o1 is Element of the U1 of C

o2 is Element of the U1 of C

<^o1,o2^> is set

o3 is Element of the U1 of C

<^o2,o3^> is set

M1 is Element of <^o1,o2^>

M2 is Element of <^o2,o3^>

M2 * M1 is Element of <^o1,o3^>

<^o1,o3^> is set

o is Element of the U1 of C

<^o1,o^> is set

<^o,o3^> is set

<^o,o2^> is set

B1 is Element of <^o,o2^>

A is Element of <^o1,o^>

B is Element of <^o,o3^>

B * A is Element of <^o1,o3^>

B2 is Element of <^o,o3^>

y is set

{y} is non empty trivial set

A1 is Element of <^o1,o^>

x is set

{x} is non empty trivial set

<^o,o^> is set

z is Element of <^o,o^>

z is set

{z} is non empty trivial set

<^o2,o^> is set

A2 is Element of <^o2,o^>

idm o is Element of <^o,o^>

A2 * B1 is Element of <^o,o^>

B2 * A2 is Element of <^o2,o3^>

B1 * A1 is Element of <^o1,o2^>

(B2 * A2) * (B1 * A1) is Element of <^o1,o3^>

(B2 * A2) * B1 is Element of <^o,o3^>

((B2 * A2) * B1) * A1 is Element of <^o1,o3^>

B * (idm o) is Element of <^o,o3^>

(B * (idm o)) * A is Element of <^o1,o3^>