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
{ b1 where b1 is Element of the carrier of Z : (Z,RR,Z,b1) } is set
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
{ b1 where b1 is Element of the carrier of Z : (Z,RR,Z,b1) } is set
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
{ b1 where b1 is Element of the carrier of Z : (Z,RR,Z,b1) } is set
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
{ [b1,b2,b3] where b1, b2, b3 is V17() V18() V19() V23() Element of NAT : ( ( b1 = b2 or b2 = b3 or b3 = b1 ) & b1 in {1,2,3} & b2 in {1,2,3} & b3 in {1,2,3} ) } is set
[:{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
{ b1 where b1 is Element of the carrier of CLSP : (CLSP,a,b,b1) } 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
{ b1 where b1 is Element of the carrier of CLSP : (CLSP,a,b,b1) } is set
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
{ b1 where b1 is Element of the carrier of CLSP : (CLSP,b,a,b1) } 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
{ b1 where b1 is Element of the carrier of CLSP : (CLSP,a,b,b1) } is set
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
{ b1 where b1 is Element of the carrier of CLSP : (CLSP,p,q,b1) } is set
r is Element of the carrier of CLSP
c18 is Element of the carrier of CLSP
c19 is Element of the carrier of CLSP
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
{ b1 where b1 is Element of the carrier of CLSP : (CLSP,a,b,b1) } is set
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
{ b1 where b1 is Element of the carrier of CLSP : (CLSP,b,p,b1) } is set
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
{ b1 where b1 is Element of the carrier of CLSP : (CLSP,a,b,b1) } is set
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
{ b1 where b1 is Element of the carrier of CLSP : (CLSP,p,q,b1) } is set
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
{ b1 where b1 is Element of the carrier of CLSP : (CLSP,a,b,b1) } is set
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
{ b1 where b1 is Element of the carrier of CLSP : (CLSP,a,b,b1) } is set
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
{ b1 where b1 is Element of the carrier of CLSP : (CLSP,a,b,b1) } is set
a is Element of the carrier of CLSP