:: COLLSP semantic presentation

REAL is set

NAT is non empty V17() V18() V19() Element of bool REAL

bool REAL is set

NAT is non empty V17() V18() V19() set

bool NAT is set

{} is empty V17() V18() V19() V21() V22() V23() set

1 is non empty V17() V18() V19() V23() Element of NAT

Z is set

[:Z,Z,Z:] is set

Z is set

the Element of Z is Element of Z

RR is set

CLS is set

{ the Element of Z} is non empty set

Z is set

RR is set

CLS is set

{CLS} is non empty set

the non empty set is non empty set

the ( the non empty set ) is ( the non empty set )

( the non empty set , the ( the non empty set )) is () ()

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

Z is non empty ()

the carrier of Z is non empty set

{1} is non empty Element of bool NAT

bool NAT is set

[1,1,1] is Element of [:NAT,NAT,NAT:]

[:NAT,NAT,NAT:] is set

{[1,1,1]} is non empty set

[:{1},{1},{1}:] is set

Z is set

Z is non empty set

RR is (Z)

(Z,RR) is () ()

CLS is non empty ()

the carrier of CLS is non empty set

the of CLS is ( the carrier of CLS)

a is Element of the carrier of CLS

b is Element of the carrier of CLS

a is Element of the carrier of CLS

[a,b,a] is Element of [: the carrier of CLS, the carrier of CLS, the carrier of CLS:]

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

Z is Element of the carrier of CLS

RR is Element of the carrier of CLS

Z is Element of the carrier of CLS

[Z,RR,Z] is Element of [: the carrier of CLS, the carrier of CLS, the carrier of CLS:]

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

RR is Element of the carrier of CLS

[Z,RR,RR] is Element of [: the carrier of CLS, the carrier of CLS, the carrier of CLS:]

CLS is Element of the carrier of CLS

[Z,RR,CLS] is Element of [: the carrier of CLS, the carrier of CLS, the carrier of CLS:]

CLSP is Element of the carrier of CLS

[Z,RR,CLSP] is Element of [: the carrier of CLS, the carrier of CLS, the carrier of CLS:]

[RR,CLS,CLSP] is Element of [: the carrier of CLS, the carrier of CLS, the carrier of CLS:]

Z is non empty () () ()

the carrier of Z is non empty set

RR is Element of the carrier of Z

Z is Element of the carrier of Z

RR is Element of the carrier of Z

[RR,Z,RR] is Element of [: the carrier of Z, the carrier of Z, the carrier of Z:]

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

the of Z is ( the carrier of Z)

Z is non empty () () ()

the carrier of Z is non empty set

RR is Element of the carrier of Z

Z is Element of the carrier of Z

RR is Element of the carrier of Z

CLS is Element of the carrier of Z

CLSP is Element of the carrier of Z

[RR,Z,CLSP] is Element of [: the carrier of Z, the carrier of Z, the carrier of Z:]

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

the of Z is ( the carrier of Z)

[RR,Z,RR] is Element of [: the carrier of Z, the carrier of Z, the carrier of Z:]

[RR,Z,CLS] is Element of [: the carrier of Z, the carrier of Z, the carrier of Z:]

[RR,CLS,CLSP] is Element of [: the carrier of Z, the carrier of Z, the carrier of Z:]

Z is non empty () () ()

the carrier of Z is non empty set

RR is Element of the carrier of Z

Z is Element of the carrier of Z

RR is Element of the carrier of Z

Z is non empty () () ()

the carrier of Z is non empty set

RR is Element of the carrier of Z

Z is Element of the carrier of Z

Z is non empty () () ()

the carrier of Z is non empty set

RR is Element of the carrier of Z

Z is Element of the carrier of Z

RR is Element of the carrier of Z

CLS is Element of the carrier of Z

Z is non empty () () ()

the carrier of Z is non empty set

RR is Element of the carrier of Z

Z is Element of the carrier of Z

RR is Element of the carrier of Z

Z is non empty () () ()

the carrier of Z is non empty set

RR is Element of the carrier of Z

Z is Element of the carrier of Z

RR is Element of the carrier of Z

Z is non empty () () ()

the carrier of Z is non empty set

RR is Element of the carrier of Z

Z is Element of the carrier of Z

RR is Element of the carrier of Z

CLS is Element of the carrier of Z

CLSP is Element of the carrier of Z

Z is non empty () () ()

the carrier of Z is non empty set

RR is Element of the carrier of Z

Z is Element of the carrier of Z

{ b

Z is non empty () () ()

the carrier of Z is non empty set

RR is Element of the carrier of Z

Z is Element of the carrier of Z

(Z,RR,Z) is set

{ b

Z is non empty () () ()

the carrier of Z is non empty set

RR is Element of the carrier of Z

Z is Element of the carrier of Z

(Z,RR,Z) is set

{ b

RR is Element of the carrier of Z

CLS is Element of the carrier of Z

2 is non empty V17() V18() V19() V23() Element of NAT

3 is non empty V17() V18() V19() V23() Element of NAT

{1,2,3} is Element of bool NAT

{ [b

[:{1,2,3},{1,2,3},{1,2,3}:] is set

Z is set

RR is V17() V18() V19() V23() Element of NAT

CLS is V17() V18() V19() V23() Element of NAT

CLSP is V17() V18() V19() V23() Element of NAT

[RR,CLS,CLSP] is Element of [:NAT,NAT,NAT:]

Z is non empty set

RR is (Z)

(Z,RR) is () ()

CLS is non empty ()

the carrier of CLS is non empty set

CLSP is Element of the carrier of CLS

a is Element of the carrier of CLS

b is Element of the carrier of CLS

[CLSP,a,b] is Element of [: the carrier of CLS, the carrier of CLS, the carrier of CLS:]

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

a is V17() V18() V19() V23() Element of NAT

b is V17() V18() V19() V23() Element of NAT

p is V17() V18() V19() V23() Element of NAT

[a,b,p] is Element of [:NAT,NAT,NAT:]

the of CLS is ( the carrier of CLS)

CLSP is Element of the carrier of CLS

a is Element of the carrier of CLS

a is Element of the carrier of CLS

[CLSP,a,a] is Element of [: the carrier of CLS, the carrier of CLS, the carrier of CLS:]

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

b is Element of the carrier of CLS

[CLSP,a,b] is Element of [: the carrier of CLS, the carrier of CLS, the carrier of CLS:]

p is Element of the carrier of CLS

[CLSP,a,p] is Element of [: the carrier of CLS, the carrier of CLS, the carrier of CLS:]

[a,b,p] is Element of [: the carrier of CLS, the carrier of CLS, the carrier of CLS:]

CLSP is Element of the carrier of CLS

a is Element of the carrier of CLS

b is Element of the carrier of CLS

[CLSP,a,b] is Element of [: the carrier of CLS, the carrier of CLS, the carrier of CLS:]

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

CLSP is Element of the carrier of CLS

a is Element of the carrier of CLS

b is Element of the carrier of CLS

[CLSP,a,b] is Element of [: the carrier of CLS, the carrier of CLS, the carrier of CLS:]

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

a is Element of the carrier of CLS

b is Element of the carrier of CLS

p is Element of the carrier of CLS

[a,b,p] is Element of [: the carrier of CLS, the carrier of CLS, the carrier of CLS:]

q is Element of the carrier of CLS

[a,b,q] is Element of [: the carrier of CLS, the carrier of CLS, the carrier of CLS:]

r is Element of the carrier of CLS

[a,b,r] is Element of [: the carrier of CLS, the carrier of CLS, the carrier of CLS:]

[p,q,r] is Element of [: the carrier of CLS, the carrier of CLS, the carrier of CLS:]

CLSP is non empty () () ()

a is Element of the carrier of CLS

b is Element of the carrier of CLS

a is Element of the carrier of CLS

CLSP is non empty () () () ()

the carrier of CLSP is non empty set

a is Element of the carrier of CLSP

b is Element of the carrier of CLSP

a is Element of the carrier of CLSP

b is Element of the carrier of CLSP

p is Element of the carrier of CLSP

CLSP is non empty () () () ()

the carrier of CLSP is non empty set

a is Element of the carrier of CLSP

b is Element of the carrier of CLSP

a is Element of the carrier of CLSP

(CLSP,a,b) is set

{ b

CLSP is non empty () () () ()

the carrier of CLSP is non empty set

a is Element of the carrier of CLSP

b is Element of the carrier of CLSP

(CLSP,a,b) is set

{ b

a is set

p is Element of the carrier of CLSP

b is Element of the carrier of CLSP

b is Element of the carrier of CLSP

CLSP is non empty () () () ()

the carrier of CLSP is non empty set

a is (CLSP)

b is Element of the carrier of CLSP

a is Element of the carrier of CLSP

(CLSP,b,a) is set

{ b

CLSP is non empty () () () ()

the carrier of CLSP is non empty set

a is Element of the carrier of CLSP

b is Element of the carrier of CLSP

(CLSP,a,b) is set

{ b

a is (CLSP)

CLSP is non empty () () () ()

the carrier of CLSP is non empty set

a is Element of the carrier of CLSP

b is Element of the carrier of CLSP

a is Element of the carrier of CLSP

b is (CLSP)

p is Element of the carrier of CLSP

q is Element of the carrier of CLSP

(CLSP,p,q) is set

{ b

r is Element of the carrier of CLSP

c

c

CLSP is non empty () () () ()

the carrier of CLSP is non empty set

a is (CLSP)

b is set

a is Element of the carrier of CLSP

b is Element of the carrier of CLSP

(CLSP,a,b) is set

{ b

p is Element of the carrier of CLSP

CLSP is non empty () () () ()

a is (CLSP)

b is (CLSP)

a is set

the carrier of CLSP is non empty set

b is Element of the carrier of CLSP

p is Element of the carrier of CLSP

(CLSP,b,p) is set

{ b

q is Element of the carrier of CLSP

CLSP is non empty () () () ()

the carrier of CLSP is non empty set

a is Element of the carrier of CLSP

b is Element of the carrier of CLSP

(CLSP,a,b) is set

{ b

a is (CLSP)

b is set

p is Element of the carrier of CLSP

q is Element of the carrier of CLSP

(CLSP,p,q) is set

{ b

r is Element of the carrier of CLSP

CLSP is non empty () () () ()

the carrier of CLSP is non empty set

a is Element of the carrier of CLSP

b is Element of the carrier of CLSP

(CLSP,a,b) is set

{ b

a is (CLSP)

b is (CLSP)

CLSP is non empty () () () ()

the carrier of CLSP is non empty set

a is Element of the carrier of CLSP

b is Element of the carrier of CLSP

a is (CLSP)

b is (CLSP)

(CLSP,a,b) is set

{ b

CLSP is non empty () () () ()

the carrier of CLSP is non empty set

a is (CLSP)

b is (CLSP)

a /\ b is set

a is set

{a} is non empty set

b is Element of the carrier of CLSP

{b} is non empty Element of bool the carrier of CLSP

bool the carrier of CLSP is set

a is set

b is set

p is Element of the carrier of CLSP

q is Element of the carrier of CLSP

a is set

{a} is non empty set

b is set

p is set

q is Element of the carrier of CLSP

{q} is non empty Element of bool the carrier of CLSP

bool the carrier of CLSP is set

CLSP is non empty () () () ()

the carrier of CLSP is non empty set

a is Element of the carrier of CLSP

b is Element of the carrier of CLSP

(CLSP,a,b) is set

{ b

a is Element of the carrier of CLSP