:: CAT_1 semantic presentation

K126() is Element of bool K122()

K122() is set

bool K122() is set

K47() is set

bool K47() is set

bool K126() is set

{} is Relation-like non-empty empty-yielding Function-like one-to-one constant functional empty trivial set

1 is non empty set

0 is Relation-like non-empty empty-yielding Function-like one-to-one constant functional empty trivial Element of K126()

{0} is functional non empty trivial set

{1} is non empty trivial set

1 :-> 0 is Relation-like {1} -defined {0} -valued Function-like non empty total V25({1},{0}) Element of bool [:{1},{0}:]

[:{1},{0}:] is Relation-like set

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

{1} --> 0 is Relation-like {1} -defined {0} -valued Function-like non empty total V25({1},{0}) Element of bool [:{1},{0}:]

(1,1) :-> 1 is Relation-like [:{1},{1}:] -defined {1} -valued Function-like total V25([:{1},{1}:],{1}) Element of bool [:[:{1},{1}:],{1}:]

[:{1},{1}:] is Relation-like set

[:[:{1},{1}:],{1}:] is Relation-like set

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

[1,1] is non empty set

{1,1} is non empty set

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

{[1,1]} is Relation-like Function-like constant non empty trivial set

{[1,1]} --> 1 is Relation-like {[1,1]} -defined {1} -valued Function-like non empty total V25({[1,1]},{1}) Element of bool [:{[1,1]},{1}:]

[:{[1,1]},{1}:] is Relation-like set

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

({0},{1},(1 :-> 0),(1 :-> 0),((1,1) :-> 1)) is () ()

C is ()

the carrier' of C is set

T is Element of the carrier' of C

D is Element of the carrier' of C

[T,D] is non empty set

{T,D} is non empty set

{T} is non empty trivial set

{{T,D},{T}} is non empty set

the of C is Relation-like [: the carrier' of C, the carrier' of C:] -defined the carrier' of C -valued Function-like Element of bool [:[: the carrier' of C, the carrier' of C:], the carrier' of C:]

[: the carrier' of C, the carrier' of C:] is Relation-like set

[:[: the carrier' of C, the carrier' of C:], the carrier' of C:] is Relation-like set

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

dom the of C is Relation-like set

the of C . (T,D) is set

the of C . [T,D] is set

C is non empty non void V59() ()

the carrier of C is non empty set

the carrier' of C is non empty set

D is Element of the carrier of C

T is Element of the carrier of C

{ b

bool the carrier' of C is set

c9 is set

f1 is Element of the carrier' of C

dom f1 is Element of the carrier of C

the Source of C is Relation-like the carrier' of C -defined the carrier of C -valued Function-like non empty total V25( the carrier' of C, the carrier of C) Element of bool [: the carrier' of C, the carrier of C:]

[: the carrier' of C, the carrier of C:] is Relation-like set

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

the Source of C . f1 is Element of the carrier of C

cod f1 is Element of the carrier of C

the Target of C is Relation-like the carrier' of C -defined the carrier of C -valued Function-like non empty total V25( the carrier' of C, the carrier of C) Element of bool [: the carrier' of C, the carrier of C:]

the Target of C . f1 is Element of the carrier of C

C is non empty non void V59() ()

the carrier' of C is non empty set

the carrier of C is non empty set

D is Element of the carrier' of C

dom D is Element of the carrier of C

the Source of C is Relation-like the carrier' of C -defined the carrier of C -valued Function-like non empty total V25( the carrier' of C, the carrier of C) Element of bool [: the carrier' of C, the carrier of C:]

[: the carrier' of C, the carrier of C:] is Relation-like set

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

the Source of C . D is Element of the carrier of C

cod D is Element of the carrier of C

the Target of C is Relation-like the carrier' of C -defined the carrier of C -valued Function-like non empty total V25( the carrier' of C, the carrier of C) Element of bool [: the carrier' of C, the carrier of C:]

the Target of C . D is Element of the carrier of C

T is Element of the carrier of C

c is Element of the carrier of C

(C,T,c) is Element of bool the carrier' of C

bool the carrier' of C is set

{ b

c9 is Element of the carrier' of C

dom c9 is Element of the carrier of C

the Source of C . c9 is Element of the carrier of C

cod c9 is Element of the carrier of C

the Target of C . c9 is Element of the carrier of C

C is non empty non void V59() ()

the carrier' of C is non empty set

D is Element of the carrier' of C

dom D is Element of the carrier of C

the carrier of C is non empty set

the Source of C is Relation-like the carrier' of C -defined the carrier of C -valued Function-like non empty total V25( the carrier' of C, the carrier of C) Element of bool [: the carrier' of C, the carrier of C:]

[: the carrier' of C, the carrier of C:] is Relation-like set

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

the Source of C . D is Element of the carrier of C

cod D is Element of the carrier of C

the Target of C is Relation-like the carrier' of C -defined the carrier of C -valued Function-like non empty total V25( the carrier' of C, the carrier of C) Element of bool [: the carrier' of C, the carrier of C:]

the Target of C . D is Element of the carrier of C

(C,(dom D),(cod D)) is Element of bool the carrier' of C

bool the carrier' of C is set

{ b

C is non empty non void V59() ()

the carrier of C is non empty set

D is Element of the carrier of C

T is Element of the carrier of C

(C,D,T) is Element of bool the carrier' of C

the carrier' of C is non empty set

bool the carrier' of C is set

{ b

C is non empty non void V59() ()

the carrier' of C is non empty set

D is Element of the carrier' of C

dom D is Element of the carrier of C

the carrier of C is non empty set

the Source of C is Relation-like the carrier' of C -defined the carrier of C -valued Function-like non empty total V25( the carrier' of C, the carrier of C) Element of bool [: the carrier' of C, the carrier of C:]

[: the carrier' of C, the carrier of C:] is Relation-like set

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

the Source of C . D is Element of the carrier of C

cod D is Element of the carrier of C

the Target of C is Relation-like the carrier' of C -defined the carrier of C -valued Function-like non empty total V25( the carrier' of C, the carrier of C) Element of bool [: the carrier' of C, the carrier of C:]

the Target of C . D is Element of the carrier of C

(C,(dom D),(cod D)) is Element of bool the carrier' of C

bool the carrier' of C is set

{ b

C is non empty non void V59() ()

the carrier of C is non empty set

D is Element of the carrier of C

T is Element of the carrier of C

(C,D,T) is Element of bool the carrier' of C

the carrier' of C is non empty set

bool the carrier' of C is set

{ b

c is (C,D,T)

dom c is Element of the carrier of C

the Source of C is Relation-like the carrier' of C -defined the carrier of C -valued Function-like non empty total V25( the carrier' of C, the carrier of C) Element of bool [: the carrier' of C, the carrier of C:]

[: the carrier' of C, the carrier of C:] is Relation-like set

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

the Source of C . c is Element of the carrier of C

cod c is Element of the carrier of C

the Target of C is Relation-like the carrier' of C -defined the carrier of C -valued Function-like non empty total V25( the carrier' of C, the carrier of C) Element of bool [: the carrier' of C, the carrier of C:]

the Target of C . c is Element of the carrier of C

C is non empty non void V59() ()

the carrier of C is non empty set

D is Element of the carrier of C

T is Element of the carrier of C

(C,D,T) is Element of bool the carrier' of C

the carrier' of C is non empty set

bool the carrier' of C is set

{ b

c is Element of the carrier of C

c9 is Element of the carrier of C

(C,c,c9) is Element of bool the carrier' of C

{ b

f1 is (C,D,T)

f2 is (C,c,c9)

dom f1 is Element of the carrier of C

the Source of C is Relation-like the carrier' of C -defined the carrier of C -valued Function-like non empty total V25( the carrier' of C, the carrier of C) Element of bool [: the carrier' of C, the carrier of C:]

[: the carrier' of C, the carrier of C:] is Relation-like set

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

the Source of C . f1 is Element of the carrier of C

cod f1 is Element of the carrier of C

the Target of C is Relation-like the carrier' of C -defined the carrier of C -valued Function-like non empty total V25( the carrier' of C, the carrier of C) Element of bool [: the carrier' of C, the carrier of C:]

the Target of C . f1 is Element of the carrier of C

C is non empty non void V59() ()

the carrier of C is non empty set

D is Element of the carrier of C

T is Element of the carrier of C

(C,D,T) is Element of bool the carrier' of C

the carrier' of C is non empty set

bool the carrier' of C is set

{ b

c is (C,D,T)

{c} is non empty trivial set

c9 is (C,D,T)

C is non empty non void V59() ()

the carrier of C is non empty set

D is Element of the carrier of C

T is Element of the carrier of C

(C,D,T) is Element of bool the carrier' of C

the carrier' of C is non empty set

bool the carrier' of C is set

{ b

c is (C,D,T)

{c} is non empty trivial set

c9 is set

f1 is Element of the carrier' of C

dom f1 is Element of the carrier of C

the Source of C is Relation-like the carrier' of C -defined the carrier of C -valued Function-like non empty total V25( the carrier' of C, the carrier of C) Element of bool [: the carrier' of C, the carrier of C:]

[: the carrier' of C, the carrier of C:] is Relation-like set

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

the Source of C . f1 is Element of the carrier of C

cod f1 is Element of the carrier of C

the Target of C is Relation-like the carrier' of C -defined the carrier of C -valued Function-like non empty total V25( the carrier' of C, the carrier of C) Element of bool [: the carrier' of C, the carrier of C:]

the Target of C . f1 is Element of the carrier of C

C is non empty non void V59() ()

the carrier of C is non empty set

D is Element of the carrier of C

T is Element of the carrier of C

(C,D,T) is Element of bool the carrier' of C

the carrier' of C is non empty set

bool the carrier' of C is set

{ b

c is Element of the carrier of C

c9 is Element of the carrier of C

(C,c,c9) is Element of bool the carrier' of C

{ b

f1 is (C,D,T)

{f1} is non empty trivial set

f2 is Relation-like Function-like set

dom f2 is set

rng f2 is set

f2 . f1 is set

{(f2 . f1)} is non empty trivial set

C is set

{C} is non empty trivial set

D is set

{D} is non empty trivial set

D :-> C is Relation-like {D} -defined {C} -valued Function-like non empty total V25({D},{C}) Element of bool [:{D},{C}:]

[:{D},{C}:] is Relation-like set

bool [:{D},{C}:] is set

{D} --> C is Relation-like {D} -defined {C} -valued Function-like non empty total V25({D},{C}) Element of bool [:{D},{C}:]

(D,D) :-> D is Relation-like [:{D},{D}:] -defined {D} -valued Function-like total V25([:{D},{D}:],{D}) Element of bool [:[:{D},{D}:],{D}:]

[:{D},{D}:] is Relation-like set

[:[:{D},{D}:],{D}:] is Relation-like set

bool [:[:{D},{D}:],{D}:] is set

[D,D] is non empty set

{D,D} is non empty set

{{D,D},{D}} is non empty set

{[D,D]} is Relation-like Function-like constant non empty trivial set

{[D,D]} --> D is Relation-like {[D,D]} -defined {D} -valued Function-like non empty total V25({[D,D]},{D}) Element of bool [:{[D,D]},{D}:]

[:{[D,D]},{D}:] is Relation-like set

bool [:{[D,D]},{D}:] is set

({C},{D},(D :-> C),(D :-> C),((D,D) :-> D)) is () ()

C is set

D is set

(C,D) is () ()

{C} is non empty trivial set

{D} is non empty trivial set

D :-> C is Relation-like {D} -defined {C} -valued Function-like non empty total V25({D},{C}) Element of bool [:{D},{C}:]

[:{D},{C}:] is Relation-like set

bool [:{D},{C}:] is set

{D} --> C is Relation-like {D} -defined {C} -valued Function-like non empty total V25({D},{C}) Element of bool [:{D},{C}:]

(D,D) :-> D is Relation-like [:{D},{D}:] -defined {D} -valued Function-like total V25([:{D},{D}:],{D}) Element of bool [:[:{D},{D}:],{D}:]

[:{D},{D}:] is Relation-like set

[:[:{D},{D}:],{D}:] is Relation-like set

bool [:[:{D},{D}:],{D}:] is set

[D,D] is non empty set

{D,D} is non empty set

{{D,D},{D}} is non empty set

{[D,D]} is Relation-like Function-like constant non empty trivial set

{[D,D]} --> D is Relation-like {[D,D]} -defined {D} -valued Function-like non empty total V25({[D,D]},{D}) Element of bool [:{[D,D]},{D}:]

[:{[D,D]},{D}:] is Relation-like set

bool [:{[D,D]},{D}:] is set

({C},{D},(D :-> C),(D :-> C),((D,D) :-> D)) is () ()

C is non empty non void V59() ()

the carrier' of C is non empty set

T is Element of the carrier' of C

dom T is Element of the carrier of C

the carrier of C is non empty set

the Source of C is Relation-like the carrier' of C -defined the carrier of C -valued Function-like non empty total V25( the carrier' of C, the carrier of C) Element of bool [: the carrier' of C, the carrier of C:]

[: the carrier' of C, the carrier of C:] is Relation-like set

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

the Source of C . T is Element of the carrier of C

D is Element of the carrier' of C

cod D is Element of the carrier of C

the Target of C is Relation-like the carrier' of C -defined the carrier of C -valued Function-like non empty total V25( the carrier' of C, the carrier of C) Element of bool [: the carrier' of C, the carrier of C:]

the Target of C . D is Element of the carrier of C

(C,D,T) is Element of the carrier' of C

dom (C,D,T) is Element of the carrier of C

the Source of C . (C,D,T) is Element of the carrier of C

dom D is Element of the carrier of C

the Source of C . D is Element of the carrier of C

cod (C,D,T) is Element of the carrier of C

the Target of C . (C,D,T) is Element of the carrier of C

cod T is Element of the carrier of C

the Target of C . T is Element of the carrier of C

the carrier of C is non empty set

D is Element of the carrier of C

(C,D,D) is Element of bool the carrier' of C

bool the carrier' of C is set

{ b

the Element of the carrier' of C is Element of the carrier' of C

cod the Element of the carrier' of C is Element of the carrier of C

the Target of C is Relation-like the carrier' of C -defined the carrier of C -valued Function-like non empty total V25( the carrier' of C, the carrier of C) Element of bool [: the carrier' of C, the carrier of C:]

[: the carrier' of C, the carrier of C:] is Relation-like set

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

the Target of C . the Element of the carrier' of C is Element of the carrier of C

dom the Element of the carrier' of C is Element of the carrier of C

the Source of C is Relation-like the carrier' of C -defined the carrier of C -valued Function-like non empty total V25( the carrier' of C, the carrier of C) Element of bool [: the carrier' of C, the carrier of C:]

the Source of C . the Element of the carrier' of C is Element of the carrier of C

C is non empty non void V59() ()

the carrier' of C is non empty set

c is Element of the carrier' of C

dom c is Element of the carrier of C

the carrier of C is non empty set

the Source of C is Relation-like the carrier' of C -defined the carrier of C -valued Function-like non empty total V25( the carrier' of C, the carrier of C) Element of bool [: the carrier' of C, the carrier of C:]

[: the carrier' of C, the carrier of C:] is Relation-like set

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

the Source of C . c is Element of the carrier of C

T is Element of the carrier' of C

cod T is Element of the carrier of C

the Target of C is Relation-like the carrier' of C -defined the carrier of C -valued Function-like non empty total V25( the carrier' of C, the carrier of C) Element of bool [: the carrier' of C, the carrier of C:]

the Target of C . T is Element of the carrier of C

dom T is Element of the carrier of C

the Source of C . T is Element of the carrier of C

D is Element of the carrier' of C

cod D is Element of the carrier of C

the Target of C . D is Element of the carrier of C

(C,D,T) is Element of the carrier' of C

(C,(C,D,T),c) is Element of the carrier' of C

(C,T,c) is Element of the carrier' of C

(C,D,(C,T,c)) is Element of the carrier' of C

the carrier of C is non empty set

D is Element of the carrier of C

the (C,D,D) is (C,D,D)

T is (C,D,D)

c is Element of the carrier of C

(C,D,c) is Element of bool the carrier' of C

bool the carrier' of C is set

{ b

(C,c,D) is Element of bool the carrier' of C

{ b

c9 is (C,D,c)

(C,T,c9) is Element of the carrier' of C

c9 is (C,c,D)

(C,c9,T) is Element of the carrier' of C

C is set

D is set

(C,D) is non empty trivial V53() non void 1 -element V59() trivial' () () () () () ()

{C} is non empty trivial set

{D} is non empty trivial set

D :-> C is Relation-like {D} -defined {C} -valued Function-like non empty total V25({D},{C}) Element of bool [:{D},{C}:]

[:{D},{C}:] is Relation-like set

bool [:{D},{C}:] is set

{D} --> C is Relation-like {D} -defined {C} -valued Function-like non empty total V25({D},{C}) Element of bool [:{D},{C}:]

(D,D) :-> D is Relation-like [:{D},{D}:] -defined {D} -valued Function-like total V25([:{D},{D}:],{D}) Element of bool [:[:{D},{D}:],{D}:]

[:{D},{D}:] is Relation-like set

[:[:{D},{D}:],{D}:] is Relation-like set

bool [:[:{D},{D}:],{D}:] is set

[D,D] is non empty set

{D,D} is non empty set

{{D,D},{D}} is non empty set

{[D,D]} is Relation-like Function-like constant non empty trivial set

{[D,D]} --> D is Relation-like {[D,D]} -defined {D} -valued Function-like non empty total V25({[D,D]},{D}) Element of bool [:{[D,D]},{D}:]

[:{[D,D]},{D}:] is Relation-like set

bool [:{[D,D]},{D}:] is set

({C},{D},(D :-> C),(D :-> C),((D,D) :-> D)) is () ()

the carrier' of (C,D) is non empty trivial set

c is Element of the carrier' of (C,D)

T is Element of the carrier' of (C,D)

[c,T] is non empty set

{c,T} is non empty set

{c} is non empty trivial set

{{c,T},{c}} is non empty set

the of (C,D) is Relation-like [: the carrier' of (C,D), the carrier' of (C,D):] -defined the carrier' of (C,D) -valued Function-like Element of bool [:[: the carrier' of (C,D), the carrier' of (C,D):], the carrier' of (C,D):]

[: the carrier' of (C,D), the carrier' of (C,D):] is Relation-like set

[:[: the carrier' of (C,D), the carrier' of (C,D):], the carrier' of (C,D):] is Relation-like set

bool [:[: the carrier' of (C,D), the carrier' of (C,D):], the carrier' of (C,D):] is set

dom the of (C,D) is Relation-like set

dom c is Element of the carrier of (C,D)

the carrier of (C,D) is non empty trivial V35() set

the Source of (C,D) is Relation-like the carrier' of (C,D) -defined the carrier of (C,D) -valued Function-like non empty total V25( the carrier' of (C,D), the carrier of (C,D)) Element of bool [: the carrier' of (C,D), the carrier of (C,D):]

[: the carrier' of (C,D), the carrier of (C,D):] is Relation-like set

bool [: the carrier' of (C,D), the carrier of (C,D):] is set

the Source of (C,D) . c is Element of the carrier of (C,D)

cod T is Element of the carrier of (C,D)

the Target of (C,D) is Relation-like the carrier' of (C,D) -defined the carrier of (C,D) -valued Function-like non empty total V25( the carrier' of (C,D), the carrier of (C,D)) Element of bool [: the carrier' of (C,D), the carrier of (C,D):]

the Target of (C,D) . T is Element of the carrier of (C,D)

0 is Relation-like non-empty empty-yielding Function-like one-to-one constant functional empty trivial Element of K126()

(0,0) is non empty trivial V53() non void 1 -element V59() trivial' () () () () () () ()

{0} is functional non empty trivial set

0 :-> 0 is Relation-like {0} -defined {0} -valued Function-like non empty total V25({0},{0}) Element of bool [:{0},{0}:]

[:{0},{0}:] is Relation-like set

bool [:{0},{0}:] is set

{0} --> 0 is Relation-like {0} -defined {0} -valued Function-like non empty total V25({0},{0}) Element of bool [:{0},{0}:]

(0,0) :-> 0 is Relation-like [:{0},{0}:] -defined {0} -valued Function-like total V25([:{0},{0}:],{0}) Element of bool [:[:{0},{0}:],{0}:]

[:[:{0},{0}:],{0}:] is Relation-like set

bool [:[:{0},{0}:],{0}:] is set

[0,0] is non empty set

{0,0} is functional non empty set

{{0,0},{0}} is non empty set

{[0,0]} is Relation-like Function-like constant non empty trivial set

{[0,0]} --> 0 is Relation-like {[0,0]} -defined {0} -valued Function-like non empty total V25({[0,0]},{0}) Element of bool [:{[0,0]},{0}:]

[:{[0,0]},{0}:] is Relation-like set

bool [:{[0,0]},{0}:] is set

({0},{0},(0 :-> 0),(0 :-> 0),((0,0) :-> 0)) is () ()

C is non empty non void V59() () ()

the carrier of C is non empty set

D is Element of the carrier of C

(C,D,D) is Element of bool the carrier' of C

the carrier' of C is non empty set

bool the carrier' of C is set

{ b

C is non empty non void V59() () () ()

the carrier of C is non empty set

D is Element of the carrier of C

T is (C,D,D)

c is (C,D,D)

(C,D,D) is non empty Element of bool the carrier' of C

the carrier' of C is non empty set

bool the carrier' of C is set

{ b

(C,c,T) is Element of the carrier' of C

C is set

D is set

(C,D) is non empty trivial V53() non void 1 -element V59() trivial' () () () () () () ()

{C} is non empty trivial set

{D} is non empty trivial set

D :-> C is Relation-like {D} -defined {C} -valued Function-like non empty total V25({D},{C}) Element of bool [:{D},{C}:]

[:{D},{C}:] is Relation-like set

bool [:{D},{C}:] is set

{D} --> C is Relation-like {D} -defined {C} -valued Function-like non empty total V25({D},{C}) Element of bool [:{D},{C}:]

(D,D) :-> D is Relation-like [:{D},{D}:] -defined {D} -valued Function-like total V25([:{D},{D}:],{D}) Element of bool [:[:{D},{D}:],{D}:]

[:{D},{D}:] is Relation-like set

[:[:{D},{D}:],{D}:] is Relation-like set

bool [:[:{D},{D}:],{D}:] is set

[D,D] is non empty set

{D,D} is non empty set

{{D,D},{D}} is non empty set

{[D,D]} is Relation-like Function-like constant non empty trivial set

{[D,D]} --> D is Relation-like {[D,D]} -defined {D} -valued Function-like non empty total V25({[D,D]},{D}) Element of bool [:{[D,D]},{D}:]

[:{[D,D]},{D}:] is Relation-like set

bool [:{[D,D]},{D}:] is set

({C},{D},(D :-> C),(D :-> C),((D,D) :-> D)) is () ()

the carrier of (C,D) is non empty trivial V35() set

the carrier' of (C,D) is non empty trivial set

T is Element of the carrier of (C,D)

c is Element of the carrier of (C,D)

((C,D),T,c) is Element of bool the carrier' of (C,D)

bool the carrier' of (C,D) is set

{ b

c9 is Element of the carrier' of (C,D)

dom c9 is Element of the carrier of (C,D)

the Source of (C,D) is Relation-like the carrier' of (C,D) -defined the carrier of (C,D) -valued Function-like non empty total V25( the carrier' of (C,D), the carrier of (C,D)) Element of bool [: the carrier' of (C,D), the carrier of (C,D):]

[: the carrier' of (C,D), the carrier of (C,D):] is Relation-like set

bool [: the carrier' of (C,D), the carrier of (C,D):] is set

the Source of (C,D) . c9 is Element of the carrier of (C,D)

cod c9 is Element of the carrier of (C,D)

the Target of (C,D) is Relation-like the carrier' of (C,D) -defined the carrier of (C,D) -valued Function-like non empty total V25( the carrier' of (C,D), the carrier of (C,D)) Element of bool [: the carrier' of (C,D), the carrier of (C,D):]

the Target of (C,D) . c9 is Element of the carrier of (C,D)

C is set

D is set

(C,D) is non empty trivial V53() non void 1 -element V59() trivial' () () () () () () ()

{C} is non empty trivial set

{D} is non empty trivial set

D :-> C is Relation-like {D} -defined {C} -valued Function-like non empty total V25({D},{C}) Element of bool [:{D},{C}:]

[:{D},{C}:] is Relation-like set

bool [:{D},{C}:] is set

{D} --> C is Relation-like {D} -defined {C} -valued Function-like non empty total V25({D},{C}) Element of bool [:{D},{C}:]

(D,D) :-> D is Relation-like [:{D},{D}:] -defined {D} -valued Function-like total V25([:{D},{D}:],{D}) Element of bool [:[:{D},{D}:],{D}:]

[:{D},{D}:] is Relation-like set

[:[:{D},{D}:],{D}:] is Relation-like set

bool [:[:{D},{D}:],{D}:] is set

[D,D] is non empty set

{D,D} is non empty set

{{D,D},{D}} is non empty set

{[D,D]} is Relation-like Function-like constant non empty trivial set

{[D,D]} --> D is Relation-like {[D,D]} -defined {D} -valued Function-like non empty total V25({[D,D]},{D}) Element of bool [:{[D,D]},{D}:]

[:{[D,D]},{D}:] is Relation-like set

bool [:{[D,D]},{D}:] is set

({C},{D},(D :-> C),(D :-> C),((D,D) :-> D)) is () ()

the carrier of (C,D) is non empty trivial V35() set

the carrier' of (C,D) is non empty trivial set

T is Element of the carrier of (C,D)

c is Element of the carrier of (C,D)

c9 is Element of the carrier' of (C,D)

((C,D),T,c) is Element of bool the carrier' of (C,D)

bool the carrier' of (C,D) is set

{ b

C is set

D is set

(C,D) is non empty trivial V53() non void 1 -element V59() trivial' () () () () () () ()

{C} is non empty trivial set

{D} is non empty trivial set

D :-> C is Relation-like {D} -defined {C} -valued Function-like non empty total V25({D},{C}) Element of bool [:{D},{C}:]

[:{D},{C}:] is Relation-like set

bool [:{D},{C}:] is set

{D} --> C is Relation-like {D} -defined {C} -valued Function-like non empty total V25({D},{C}) Element of bool [:{D},{C}:]

(D,D) :-> D is Relation-like [:{D},{D}:] -defined {D} -valued Function-like total V25([:{D},{D}:],{D}) Element of bool [:[:{D},{D}:],{D}:]

[:{D},{D}:] is Relation-like set

[:[:{D},{D}:],{D}:] is Relation-like set

bool [:[:{D},{D}:],{D}:] is set

[D,D] is non empty set

{D,D} is non empty set

{{D,D},{D}} is non empty set

{[D,D]} is Relation-like Function-like constant non empty trivial set

{[D,D]} --> D is Relation-like {[D,D]} -defined {D} -valued Function-like non empty total V25({[D,D]},{D}) Element of bool [:{[D,D]},{D}:]

[:{[D,D]},{D}:] is Relation-like set

bool [:{[D,D]},{D}:] is set

({C},{D},(D :-> C),(D :-> C),((D,D) :-> D)) is () ()

the carrier of (C,D) is non empty trivial V35() set

T is Element of the carrier of (C,D)

c is Element of the carrier of (C,D)

((C,D),T,c) is Element of bool the carrier' of (C,D)

the carrier' of (C,D) is non empty trivial set

bool the carrier' of (C,D) is set

{ b

C is set

D is set

(C,D) is non empty trivial V53() non void 1 -element V59() trivial' () () () () () () ()

{C} is non empty trivial set

{D} is non empty trivial set

D :-> C is Relation-like {D} -defined {C} -valued Function-like non empty total V25({D},{C}) Element of bool [:{D},{C}:]

[:{D},{C}:] is Relation-like set

bool [:{D},{C}:] is set

{D} --> C is Relation-like {D} -defined {C} -valued Function-like non empty total V25({D},{C}) Element of bool [:{D},{C}:]

(D,D) :-> D is Relation-like [:{D},{D}:] -defined {D} -valued Function-like total V25([:{D},{D}:],{D}) Element of bool [:[:{D},{D}:],{D}:]

[:{D},{D}:] is Relation-like set

[:[:{D},{D}:],{D}:] is Relation-like set

bool [:[:{D},{D}:],{D}:] is set

[D,D] is non empty set

{D,D} is non empty set

{{D,D},{D}} is non empty set

{[D,D]} is Relation-like Function-like constant non empty trivial set

{[D,D]} --> D is Relation-like {[D,D]} -defined {D} -valued Function-like non empty total V25({[D,D]},{D}) Element of bool [:{[D,D]},{D}:]

[:{[D,D]},{D}:] is Relation-like set

bool [:{[D,D]},{D}:] is set

({C},{D},(D :-> C),(D :-> C),((D,D) :-> D)) is () ()

the carrier of (C,D) is non empty trivial V35() set

T is Element of the carrier of (C,D)

c is Element of the carrier of (C,D)

c9 is Element of the carrier of (C,D)

f1 is Element of the carrier of (C,D)

f2 is ((C,D),T,c)

f is ((C,D),c9,f1)

C is non empty non void V59() () () () () () ()

the carrier' of C is non empty set

c is non empty non void V59() () () () () () ()

the carrier' of c is non empty set

D is Element of the carrier' of C

dom D is Element of the carrier of C

the carrier of C is non empty set

the Source of C is Relation-like the carrier' of C -defined the carrier of C -valued Function-like non empty total V25( the carrier' of C, the carrier of C) Element of bool [: the carrier' of C, the carrier of C:]

[: the carrier' of C, the carrier of C:] is Relation-like set

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

the Source of C . D is Element of the carrier of C

T is Element of the carrier' of C

cod T is Element of the carrier of C

the Target of C is Relation-like the carrier' of C -defined the carrier of C -valued Function-like non empty total V25( the carrier' of C, the carrier of C) Element of bool [: the carrier' of C, the carrier of C:]

the Target of C . T is Element of the carrier of C

[D,T] is non empty set

{D,T} is non empty set

{D} is non empty trivial set

{{D,T},{D}} is non empty set

the of C is Relation-like [: the carrier' of C, the carrier' of C:] -defined the carrier' of C -valued Function-like Element of bool [:[: the carrier' of C, the carrier' of C:], the carrier' of C:]

[: the carrier' of C, the carrier' of C:] is Relation-like set

[:[: the carrier' of C, the carrier' of C:], the carrier' of C:] is Relation-like set

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

dom the of C is Relation-like set

c9 is Element of the carrier' of c

f1 is Element of the carrier' of c

[c9,f1] is non empty set

{c9,f1} is non empty set

{c9} is non empty trivial set

{{c9,f1},{c9}} is non empty set

the of c is Relation-like [: the carrier' of c, the carrier' of c:] -defined the carrier' of c -valued Function-like Element of bool [:[: the carrier' of c, the carrier' of c:], the carrier' of c:]

[: the carrier' of c, the carrier' of c:] is Relation-like set

[:[: the carrier' of c, the carrier' of c:], the carrier' of c:] is Relation-like set

bool [:[: the carrier' of c, the carrier' of c:], the carrier' of c:] is set

dom the of c is Relation-like set

dom c9 is Element of the carrier of c

the carrier of c is non empty set

the Source of c is Relation-like the carrier' of c -defined the carrier of c -valued Function-like non empty total V25( the carrier' of c, the carrier of c) Element of bool [: the carrier' of c, the carrier of c:]

[: the carrier' of c, the carrier of c:] is Relation-like set

bool [: the carrier' of c, the carrier of c:] is set

the Source of c . c9 is Element of the carrier of c

cod f1 is Element of the carrier of c

the Target of c is Relation-like the carrier' of c -defined the carrier of c -valued Function-like non empty total V25( the carrier' of c, the carrier of c) Element of bool [: the carrier' of c, the carrier of c:]

the Target of c . f1 is Element of the carrier of c

C is non empty non void V59() () () () () () ()

the carrier' of C is non empty set

the of C is Relation-like [: the carrier' of C, the carrier' of C:] -defined the carrier' of C -valued Function-like Element of bool [:[: the carrier' of C, the carrier' of C:], the carrier' of C:]

[: the carrier' of C, the carrier' of C:] is Relation-like set

[:[: the carrier' of C, the carrier' of C:], the carrier' of C:] is Relation-like set

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

D is Element of the carrier' of C

dom D is Element of the carrier of C

the carrier of C is non empty set

the Source of C is Relation-like the carrier' of C -defined the carrier of C -valued Function-like non empty total V25( the carrier' of C, the carrier of C) Element of bool [: the carrier' of C, the carrier of C:]

[: the carrier' of C, the carrier of C:] is Relation-like set

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

the Source of C . D is Element of the carrier of C

T is Element of the carrier' of C

cod T is Element of the carrier of C

the Target of C is Relation-like the carrier' of C -defined the carrier of C -valued Function-like non empty total V25( the carrier' of C, the carrier of C) Element of bool [: the carrier' of C, the carrier of C:]

the Target of C . T is Element of the carrier of C

(C,T,D) is Element of the carrier' of C

the of C . (D,T) is set

[D,T] is non empty set

{D,T} is non empty set

{D} is non empty trivial set

{{D,T},{D}} is non empty set

the of C . [D,T] is set

dom the of C is Relation-like set

C is non empty non void V59() () () () () () ()

the carrier' of C is non empty set

T is Element of the carrier' of C

dom T is Element of the carrier of C

the carrier of C is non empty set

the Source of C is Relation-like the carrier' of C -defined the carrier of C -valued Function-like non empty total V25( the carrier' of C, the carrier of C) Element of bool [: the carrier' of C, the carrier of C:]

[: the carrier' of C, the carrier of C:] is Relation-like set

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

the Source of C . T is Element of the carrier of C

D is Element of the carrier' of C

cod D is Element of the carrier of C

the Target of C is Relation-like the carrier' of C -defined the carrier of C -valued Function-like non empty total V25( the carrier' of C, the carrier of C) Element of bool [: the carrier' of C, the carrier of C:]

the Target of C . D is Element of the carrier of C

(C,D,T) is Element of the carrier' of C

dom (C,D,T) is Element of the carrier of C

the Source of C . (C,D,T) is Element of the carrier of C

dom D is Element of the carrier of C

the Source of C . D is Element of the carrier of C

cod (C,D,T) is Element of the carrier of C

the Target of C . (C,D,T) is Element of the carrier of C

cod T is Element of the carrier of C

the Target of C . T is Element of the carrier of C

C is non empty non void V59() () () () () () ()

the carrier' of C is non empty set

c is Element of the carrier' of C

dom c is Element of the carrier of C

the carrier of C is non empty set

the Source of C is Relation-like the carrier' of C -defined the carrier of C -valued Function-like non empty total V25( the carrier' of C, the carrier of C) Element of bool [: the carrier' of C, the carrier of C:]

[: the carrier' of C, the carrier of C:] is Relation-like set

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

the Source of C . c is Element of the carrier of C

T is Element of the carrier' of C

cod T is Element of the carrier of C

the Target of C is Relation-like the carrier' of C -defined the carrier of C -valued Function-like non empty total V25( the carrier' of C, the carrier of C) Element of bool [: the carrier' of C, the carrier of C:]

the Target of C . T is Element of the carrier of C

dom T is Element of the carrier of C

the Source of C . T is Element of the carrier of C

D is Element of the carrier' of C

cod D is Element of the carrier of C

the Target of C . D is Element of the carrier of C

(C,D,T) is Element of the carrier' of C

(C,(C,D,T),c) is Element of the carrier' of C

(C,T,c) is Element of the carrier' of C

(C,D,(C,T,c)) is Element of the carrier' of C

C is non empty non void V59() () () () () () ()

the carrier of C is non empty set

the carrier' of C is non empty set

D is Element of the carrier of C

(C,D) is (C,D,D)

T is Element of the carrier' of C

cod T is Element of the carrier of C

the Target of C is Relation-like the carrier' of C -defined the carrier of C -valued Function-like non empty total V25( the carrier' of C, the carrier of C) Element of bool [: the carrier' of C, the carrier of C:]

[: the carrier' of C, the carrier of C:] is Relation-like set

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

the Target of C . T is Element of the carrier of C

(C,T,(C,D)) is Element of the carrier' of C

dom T is Element of the carrier of C

the Source of C is Relation-like the carrier' of C -defined the carrier of C -valued Function-like non empty total V25( the carrier' of C, the carrier of C) Element of bool [: the carrier' of C, the carrier of C:]

the Source of C . T is Element of the carrier of C

(C,(dom T),D) is Element of bool the carrier' of C

bool the carrier' of C is set

{ b

c is (C, dom T,D)

(C,c,(C,D)) is Element of the carrier' of C

C is non empty non void V59() () () () () () ()

the carrier of C is non empty set

the carrier' of C is non empty set

D is Element of the carrier of C

(C,D) is (C,D,D)

T is Element of the carrier' of C

dom T is Element of the carrier of C

the Source of C is Relation-like the carrier' of C -defined the carrier of C -valued Function-like non empty total V25( the carrier' of C, the carrier of C) Element of bool [: the carrier' of C, the carrier of C:]

[: the carrier' of C, the carrier of C:] is Relation-like set

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

the Source of C . T is Element of the carrier of C

(C,(C,D),T) is Element of the carrier' of C

cod T is Element of the carrier of C

the Target of C is Relation-like the carrier' of C -defined the carrier of C -valued Function-like non empty total V25( the carrier' of C, the carrier of C) Element of bool [: the carrier' of C, the carrier of C:]

the Target of C . T is Element of the carrier of C

(C,D,(cod T)) is Element of bool the carrier' of C

bool the carrier' of C is set

{ b

c is (C,D, cod T)

(C,(C,D),c) is Element of the carrier' of C

C is non empty non void V59() () () () () () ()

the carrier of C is non empty set

D is Element of the carrier of C

T is Element of the carrier of C

(C,D,T) is Element of bool the carrier' of C

the carrier' of C is non empty set

bool the carrier' of C is set

{ b

c is Element of the carrier of C

(C,T,c) is Element of bool the carrier' of C

{ b

(C,D,c) is Element of bool the carrier' of C

{ b

c9 is (C,D,T)

f1 is (C,T,c)

(C,c9,f1) is Element of the carrier' of C

cod c9 is Element of the carrier of C

the Target of C is Relation-like the carrier' of C -defined the carrier of C -valued Function-like non empty total V25( the carrier' of C, the carrier of C) Element of bool [: the carrier' of C, the carrier of C:]

[: the carrier' of C, the carrier of C:] is Relation-like set

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

the Target of C . c9 is Element of the carrier of C

dom f1 is Element of the carrier of C

the Source of C is Relation-like the carrier' of C -defined the carrier of C -valued Function-like non empty total V25( the carrier' of C, the carrier of C) Element of bool [: the carrier' of C, the carrier of C:]

the Source of C . f1 is Element of the carrier of C

cod f1 is Element of the carrier of C

the Target of C . f1 is Element of the carrier of C

cod (C,c9,f1) is Element of the carrier of C

the Target of C . (C,c9,f1) is Element of the carrier of C

dom c9 is Element of the carrier of C

the Source of C . c9 is Element of the carrier of C

dom (C,c9,f1) is Element of the carrier of C

the Source of C . (C,c9,f1) is Element of the carrier of C

C is non empty non void V59() () () () () () ()

the carrier of C is non empty set

D is Element of the carrier of C

T is Element of the carrier of C

c is Element of the carrier of C

(C,D,T) is Element of bool the carrier' of C

the carrier' of C is non empty set

bool the carrier' of C is set

{ b

(C,T,c) is Element of bool the carrier' of C

{ b

c9 is (C,D,T)

f1 is (C,T,c)

(C,c9,f1) is Element of the carrier' of C

(C,D,c) is Element of bool the carrier' of C

{ b

C is non empty non void V59() () () () () () ()

the carrier of C is non empty set

D is Element of the carrier of C

T is Element of the carrier of C

(C,D,T) is Element of bool the carrier' of C

the carrier' of C is non empty set

bool the carrier' of C is set

{ b

c is Element of the carrier of C

(C,T,c) is Element of bool the carrier' of C

{ b

(C,D,c) is Element of bool the carrier' of C

{ b

C is non empty non void V59() () () () () () ()

the carrier of C is non empty set

D is Element of the carrier of C

T is Element of the carrier of C

(C,D,T) is Element of bool the carrier' of C

the carrier' of C is non empty set

bool the carrier' of C is set

{ b

c is Element of the carrier of C

(C,T,c) is Element of bool the carrier' of C

{ b

c9 is Element of the carrier of C

(C,c,c9) is Element of bool the carrier' of C

{ b

f1 is (C,D,T)

f2 is (C,T,c)

(C,D,T,c,f1,f2) is (C,D,c)

f is (C,c,c9)

(C,T,c,c9,f2,f) is (C,T,c9)

(C,D,T,c9,f1,(C,T,c,c9,f2,f)) is (C,D,c9)

(C,D,c,c9,(C,D,T,c,f1,f2),f) is (C,D,c9)

(C,D,c) is Element of bool the carrier' of C

{ b

dom f is Element of the carrier of C

the Source of C is Relation-like the carrier' of C -defined the carrier of C -valued Function-like non empty total V25( the carrier' of C, the carrier of C) Element of bool [: the carrier' of C, the carrier of C:]

[: the carrier' of C, the carrier of C:] is Relation-like set

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

the Source of C . f is Element of the carrier of C

cod f2 is Element of the carrier of C

the Target of C is Relation-like the carrier' of C -defined the carrier of C -valued Function-like non empty total V25( the carrier' of C, the carrier of C) Element of bool [: the carrier' of C, the carrier of C:]

the Target of C . f2 is Element of the carrier of C

dom f2 is Element of the carrier of C

the Source of C . f2 is Element of the carrier of C

cod f1 is Element of the carrier of C

the Target of C . f1 is Element of the carrier of C

(C,T,c9) is Element of bool the carrier' of C

{ b

c

(C,c

h is Element of the carrier' of C

c

(C,h,c

(C,c

(C,c

(C,(C,c

(C,(C,D,T,c,f1,f2),c

C is non empty non void V59() () () () () () ()

the carrier of C is non empty set

D is Element of the carrier of C

(C,D) is (C,D,D)

(C,D,D) is non empty Element of bool the carrier' of C

the carrier' of C is non empty set

bool the carrier' of C is set

{ b

C is non empty non void V59() () () () () () ()

the carrier of C is non empty set

D is Element of the carrier of C

T is Element of the carrier of C

(C,D,T) is Element of bool the carrier' of C

the carrier' of C is non empty set

bool the carrier' of C is set

{ b

(C,T) is (C,T,T)

c is (C,D,T)

(C,D,T,T,c,(C,T)) is (C,D,T)

(C,c,(C,T)) is Element of the carrier' of C

(C,T,T) is non empty Element of bool the carrier' of C

{ b

C is non empty non void V59() () () () () () ()

the carrier of C is non empty set

D is Element of the carrier of C

(C,D) is (C,D,D)

T is Element of the carrier of C

(C,D,T) is Element of bool the carrier' of C

the carrier' of C is non empty set

bool the carrier' of C is set

{ b

c is (C,D,T)

(C,D,D,T,(C,D),c) is (C,D,T)

(C,(C,D),c) is Element of the carrier' of C

(C,D,D) is non empty Element of bool the carrier' of C

{ b

C is non empty non void V59() () () () () () ()

the carrier of C is non empty set

D is Element of the carrier of C

(C,D,D) is non empty Element of bool the carrier' of C

the carrier' of C is non empty set

bool the carrier' of C is set

{ b

(C,D) is (C,D,D)

T is (C,D,D)

(C,D,D,D,(C,D),T) is (C,D,D)

(C,D,D,D,T,(C,D)) is (C,D,D)

C is non empty non void V59() () () () () () ()

the carrier of C is non empty set

D is Element of the carrier of C

(C,D) is (C,D,D)

(C,D,D,D,(C,D),(C,D)) is (C,D,D)

C is non empty non void V59() () () () () () ()

the carrier of C is non empty set

D is Element of the carrier of C

T is Element of the carrier of C

C is non empty non void V59() () () () () () ()

the carrier of C is non empty set

D is Element of the carrier of C

T is Element of the carrier of C

C is non empty non void V59() () () () () () ()

the carrier of C is non empty set

D is Element of the carrier of C

T is Element of the carrier of C

C is non empty non void V59() () () () () () ()

the carrier of C is non empty set

D is Element of the carrier of C

T is Element of the carrier of C

(C,D,T) is Element of bool the carrier' of C

the carrier' of C is non empty set

bool the carrier' of C is set

{ b

c is (C,D,T)

c9 is Element of the carrier of C

(C,c9,D) is Element of bool the carrier' of C

{ b

f1 is (C,c9,D)

(C,c9,D,T,f1,c) is (C,c9,T)

f2 is (C,c9,D)

(C,c9,D,T,f2,c) is (C,c9,T)

c9 is Element of the carrier of C

(C,c9,D) is Element of bool the carrier' of C

{ b

f1 is (C,c9,D)

(C,c9,D,T,f1,c) is (C,c9,T)

f2 is (C,c9,D)

(C,c9,D,T,f2,c) is (C,c9,T)

C is non empty non void V59() () () () () () ()

the carrier of C is non empty set

D is Element of the carrier of C

T is Element of the carrier of C

c is Element of the carrier of C

c9 is (C,D,T)

f1 is (C,T,c)

(C,D,T,c,c9,f1) is (C,D,c)

(C,D,T) is Element of bool the carrier' of C

the carrier' of C is non empty set

bool the carrier' of C is set

{ b

(C,T,c) is Element of bool the carrier' of C

{ b

f2 is Element of the carrier of C

(C,f2,D) is Element of bool the carrier' of C

{ b

f is (C,f2,D)

(C,f2,D,c,f,(C,D,T,c,c9,f1)) is (C,f2,c)

c

(C,f2,D,c,c

(C,f2,T) is Element of bool the carrier' of C

{ b

(C,f2,D,T,f,c9) is (C,f2,T)

(C,f2,T,c,(C,f2,D,T,f,c9),f1) is (C,f2,c)

(C,f2,D,T,c

(C,f2,T,c,(C,f2,D,T,c

(C,D,c) is Element of bool the carrier' of C

{ b

C is non empty non void V59() () () () () () ()

the carrier of C is non empty set

D is Element of the carrier of C

T is Element of the carrier of C

(C,D,T) is Element of bool the carrier' of C

the carrier' of C is non empty set

bool the carrier' of C is set

{ b

c is Element of the carrier of C

(C,T,c) is Element of bool the carrier' of C

{ b

c9 is (C,D,T)

f1 is (C,T,c)

(C,D,T,c,c9,f1) is (C,D,c)

f2 is Element of the carrier of C

(C,D,c) is Element of bool the carrier' of C

{ b

(C,f2,D) is Element of bool the carrier' of C

{ b

f is (C,f2,D)

(C,f2,D,T,f,c9) is (C,f2,T)

(C,f2,T,c,(C,f2,D,T,f,c9),f1) is (C,f2,c)

(C,f2,D,c,f,(C,D,T,c,c9,f1)) is (C,f2,c)

c

(C,f2,D,T,c

(C,f2,T,c,(C,f2,D,T,c

(C,f2,D,c,c

C is non empty non void V59() () () () () () ()

the carrier of C is non empty set

D is Element of the carrier of C

T is Element of the carrier of C

(C,D,T) is Element of bool the carrier' of C

the carrier' of C is non empty set

bool the carrier' of C is set

{ b

(C,T,D) is Element of bool the carrier' of C

{ b

(C,T) is (C,T,T)

c is (C,D,T)

c9 is (C,T,D)

(C,T,D,T,c9,c) is (C,T,T)

f1 is Element of the carrier of C

(C,f1,T) is Element of bool the carrier' of C

{ b

f2 is (C,f1,T)

(C,f1,T,D,f2,c9) is (C,f1,D)

f is (C,f1,T)

(C,f1,T,D,f,c9) is (C,f1,D)

(C,f1,T,T,f2,(C,T,D,T,c9,c)) is (C,f1,T)

(C,f1,D,T,(C,f1,T,D,f,c9),c) is (C,f1,T)

(C,f1,T,T,f,(C,T,D,T,c9,c)) is (C,f1,T)

C is non empty non void V59() () () () () () ()

the carrier of C is non empty set

D is Element of the carrier of C

(C,D) is (C,D,D)

T is Element of the carrier of C

(C,T,D) is Element of bool the carrier' of C

the carrier' of C is non empty set

bool the carrier' of C is set

{ b

c is (C,T,D)

(C,T,D,D,c,(C,D)) is (C,T,D)

c9 is (C,T,D)

(C,T,D,D,c9,(C,D)) is (C,T,D)

(C,D,D) is non empty Element of bool the carrier' of C

{ b

C is non empty non void V59() () () () () () ()

the carrier of C is non empty set

D is Element of the carrier of C

T is Element of the carrier of C

(C,D,T) is Element of bool the carrier' of C

the carrier' of C is non empty set

bool the carrier' of C is set

{ b

c is (C,D,T)

c9 is Element of the carrier of C

(C,T,c9) is Element of bool the carrier' of C

{ b

f1 is (C,T,c9)

(C,D,T,c9,c,f1) is (C,D,c9)

f2 is (C,T,c9)

(C,D,T,c9,c,f2) is (C,D,c9)

c9 is Element of the carrier of C

(C,T,c9) is Element of bool the carrier' of C

{ b

f1 is (C,T,c9)

(C,D,T,c9,c,f1) is (C,D,c9)

f2 is (C,T,c9)

(C,D,T,c9,c,f2) is (C,D,c9)

C is non empty non void V59() () () () () () ()

the carrier of C is non empty set

D is Element of the carrier of C

T is Element of the carrier of C

c is Element of the carrier of C

c9 is (C,D,T)

f1 is (C,T,c)

(C,D,T,c,c9,f1) is (C,D,c)

(C,D,T) is Element of bool the carrier' of C

the carrier' of C is non empty set

bool the carrier' of C is set

{ b

(C,T,c) is Element of bool the carrier' of C

{ b

f2 is Element of the carrier of C

(C,c,f2) is Element of bool the carrier' of C

{ b

f is (C,c,f2)

(C,D,c,f2,(C,D,T,c,c9,f1),f) is (C,D,f2)

c

(C,D,c,f2,(C,D,T,c,c9,f1),c

(C,T,f2) is Element of bool the carrier' of C

{ b

(C,T,c,f2,f1,f) is (C,T,f2)

(C,D,T,f2,c9,(C,T,c,f2,f1,f)) is (C,D,f2)

(C,T,c,f2,f1,c

(C,D,T,f2,c9,(C,T,c,f2,f1,c

(C,D,c) is Element of bool the carrier' of C

{ b

C is non empty non void V59() () () () () () ()

the carrier of C is non empty set

D is Element of the carrier of C

T is Element of the carrier of C

(C,D,T) is Element of bool the carrier' of C

the carrier' of C is non empty set

bool the carrier' of C is set

{ b

c is Element of the carrier of C

(C,T,c) is Element of bool the carrier' of C

{ b

c9 is (C,D,T)

f1 is (C,T,c)

(C,D,T,c,c9,f1) is (C,D,c)

f2 is Element of the carrier of C

(C,D,c) is Element of bool the carrier' of C

{ b

(C,c,f2) is Element of bool the carrier' of C

{ b

f is (C,c,f2)

(C,D,c,f2,(C,D,T,c,c9,f1),f) is (C,D,f2)

(C,T,c,f2,f1,f) is (C,T,f2)

(C,D,T,f2,c9,(C,T,c,f2,f1,f)) is (C,D,f2)

c

(C,D,c,f2,(C,D,T,c,c9,f1),c

(C,T,c,f2,f1,c

(C,D,T,f2,c9,(C,T,c,f2,f1,c

C is non empty non void V59() () () () () () ()

the carrier of C is non empty set

D is Element of the carrier of C

T is Element of the carrier of C

(C,D,T) is Element of bool the carrier' of C

the carrier' of C is non empty set

bool the carrier' of C is set

{ b

(C,T,D) is Element of bool the carrier' of C

{ b

(C,T) is (C,T,T)

c is (C,D,T)

c9 is (C,T,D)

(C,T,D,T,c9,c) is (C,T,T)

f1 is Element of the carrier of C

(C,T,f1) is Element of bool the carrier' of C

{ b

f2 is (C,T,f1)

(C,D,T,f1,c,f2) is (C,D,f1)

f is (C,T,f1)

(C,D,T,f1,c,f) is (C,D,f1)

(C,T,T,f1,(C,T,D,T,c9,c),f2) is (C,T,f1)

(C,T,D,f1,c9,(C,D,T,f1,c,f)) is (C,T,f1)

(C,T,T,f1,(C,T,D,T,c9,c),f) is (C,T,f1)

C is non empty non void V59() () () () () () ()

the carrier of C is non empty set

D is Element of the carrier of C

(C,D) is (C,D,D)

T is Element of the carrier of C

(C,D,T) is Element of bool the carrier' of C

the carrier' of C is non empty set

bool the carrier' of C is set

{ b

c is (C,D,T)

(C,D,D,T,(C,D),c) is (C,D,T)

c9 is (C,D,T)

(C,D,D,T,(C,D),c9) is (C,D,T)

(C,D,D) is non empty Element of bool the carrier' of C

{ b

C is non empty non void V59() () () () () () ()

the carrier of C is non empty set

D is Element of the carrier of C

(C,D) is (C,D,D)

T is Element of the carrier of C

(C,D,T) is Element of bool the carrier' of C

the carrier' of C is non empty set

bool the carrier' of C is set

{ b

(C,T,D) is Element of bool the carrier' of C

{ b

(C,T) is (C,T,T)

c is (C,D,T)

c9 is (C,T,D)

(C,T,D,T,c9,c) is (C,T,T)

(C,D,T,D,c,c9) is (C,D,D)

c9 is (C,T,D)

(C,T,D,T,c9,c) is (C,T,T)

(C,D,T,D,c,c9) is (C,D,D)

C is non empty non void V59() () () () () () ()

the carrier of C is non empty set

D is Element of the carrier of C

(C,D) is (C,D,D)

T is Element of the carrier of C

(C,D,T) is Element of bool the carrier' of C

the carrier' of C is non empty set

bool the carrier' of C is set

{ b

(C,T,D) is Element of bool the carrier' of C

{ b

(C,T) is (C,T,T)

c is (C,D,T)

c9 is (C,T,D)

(C,T,D,T,c9,c) is (C,T,T)

f1 is (C,T,D)

(C,D,T,D,c,f1) is (C,D,D)

(C,T,D,D,c9,(C,D,T,D,c,f1)) is (C,T,D)

(C,T,T,D,(C,T),f1) is (C,T,D)

C is non empty non void V59() () () () () () ()

the carrier of C is non empty set

D is Element of the carrier of C

T is Element of the carrier of C

c is (C,D,T)

(C,D,T) is Element of bool the carrier' of C

the carrier' of C is non empty set

bool the carrier' of C is set

{ b

(C,T) is (C,T,T)

(C,D) is (C,D,D)

(C,T,D) is Element of bool the carrier' of C

{ b

c9 is (C,T,D)

(C,T,D,T,c9,c) is (C,T,T)

(C,D,T,D,c,c9) is (C,D,D)

f1 is (C,T,D)

(C,T,D,T,f1,c) is (C,T,T)

(C,D,T,D,c,f1) is (C,D,D)

C is non empty non void V59() () () () () () ()

the carrier of C is non empty set

D is Element of the carrier of C

T is Element of the carrier of C

c is (C,D,T)

(C,D,T) is Element of bool the carrier' of C

the carrier' of C is non empty set

bool the carrier' of C is set

{ b

(C,T) is (C,T,T)

(C,D) is (C,D,D)

c9 is (C,T,D)

(C,T,D,T,c9,c) is (C,T,T)

(C,D,T,D,c,c9) is (C,D,D)

(C,T,D) is Element of bool the carrier' of C

{ b

f1 is Element of the carrier of C

(C,f1,D) is Element of bool the carrier' of C

{ b

f2 is (C,f1,D)

(C,f1,D,T,f2,c) is (C,f1,T)

f is (C,f1,D)

(C,f1,D,T,f,c) is (C,f1,T)

(C,f1,D,D,f2,(C,D,T,D,c,c9)) is (C,f1,D)

(C,f1,T,D,(C,f1,D,T,f,c),c9) is (C,f1,D)

(C,f1,D,D,f,(C,D)) is (C,f1,D)

f1 is Element of the carrier of C

(C,T,f1) is Element of bool the carrier' of C

{ b

f2 is (C,T,f1)

(C,D,T,f1,c,f2) is (C,D,f1)

f is (C,T,f1)

(C,D,T,f1,c,f) is (C,D,f1)

(C,T,T,f1,(C,T,D,T,c9,c),f2) is (C,T,f1)

(C,T,D,f1,c9,(C,D,T,f1,c,f)) is (C,T,f1)

(C,T,T,f1,(C,T),f) is (C,T,f1)

C is non empty non void V59() () () () () () ()

the carrier of C is non empty set

D is Element of the carrier of C

(C,D) is (C,D,D)

(C,D,D) is non empty Element of bool the carrier' of C

the carrier' of C is non empty set

bool the carrier' of C is set

{ b

(C,D,D,D,(C,D),(C,D)) is (C,D,D)

C is non empty non void V59() () () () () () ()

the carrier of C is non empty set

D is Element of the carrier of C

T is Element of the carrier of C

c is Element of the carrier of C

c9 is (C,D,T)

f1 is (C,T,c)

(C,D,T,c,c9,f1) is (C,D,c)

(C,D,T) is Element of bool the carrier' of C

the carrier' of C is non empty set

bool the carrier' of C is set

{ b

(C,T,D) is Element of bool the carrier' of C

{ b

(C,T) is (C,T,T)

(C,D) is (C,D,D)

f2 is (C,T,D)

(C,T,D,T,f2,c9) is (C,T,T)

(C,D,T,D,c9,f2) is (C,D,D)

(C,T,c) is Element of bool the carrier' of C

{ b

(C,c,T) is Element of bool the carrier' of C

{ b

(C,c) is (C,c,c)

f is (C,c,T)

(C,c,T,c,f,f1) is (C,c,c)

(C,T,c,T,f1,f) is (C,T,T)

(C,c,D) is Element of bool the carrier' of C

{ b

(C,c,T,D,f,f2) is (C,c,D)

c

(C,c,D,c,c

(C,c,D,T,(C,c,T,D,f,f2),c9) is (C,c,T)

(C,c,T,c,(C,c,D,T,(C,c,T,D,f,f2),c9),f1) is (C,c,c)

(C,c,T,T,f,(C,T)) is (C,c,T)

(C,c,T,c,(C,c,T,T,f,(C,T)),f1) is (C,c,c)

(C,D,c) is Element of bool the carrier' of C

{ b

(C,D,c,D,(C,D,T,c,c9,f1),c

(C,D,c,T,(C,D,T,c,c9,f1),f) is (C,D,T)

(C,D,T,D,(C,D,c,T,(C,D,T,c,c9,f1),f),f2) is (C,D,D)

(C,D,T,T,c9,(C,T)) is (C,D,T)

(C,D,T,D,(C,D,T,T,c9,(C,T)),f2) is (C,D,D)

c

(C,c,D,c,c

(C,D,c,D,(C,D,T,c,c9,f1),c

C is non empty non void V59() () () () () () ()

the carrier of C is non empty set

D is Element of the carrier of C

T is Element of the carrier of C

c is (C,D,T)

(C,D,T,c) is (C,T,D)

(C,T,D,T,(C,D,T,c),c) is (C,T,T)

(C,T) is (C,T,T)

(C,D,T) is Element of bool the carrier' of C<