:: FIN_TOPO semantic presentation

REAL is set

NAT is non empty epsilon-transitive epsilon-connected ordinal Element of K32(REAL)

K32(REAL) is non empty set

COMPLEX is set

omega is non empty epsilon-transitive epsilon-connected ordinal set

K32(omega) is non empty set

K32(NAT) is non empty set

{} is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V30() V31() V32() finite V50() ext-real non positive non negative set

the empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V30() V31() V32() finite V50() ext-real non positive non negative set is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V30() V31() V32() finite V50() ext-real non positive non negative set

1 is non empty epsilon-transitive epsilon-connected ordinal natural V30() V31() V32() ext-real positive non negative Element of NAT

0 is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V30() V31() V32() finite V50() ext-real non positive non negative Element of NAT

FT is set

bool FT is non empty Element of K32(K32(FT))

K32(FT) is non empty set

K32(K32(FT)) is non empty set

A is V7() V10( NAT ) V11( bool FT) Function-like FinSequence-like FinSequence of bool FT

len A is epsilon-transitive epsilon-connected ordinal natural V30() V31() V32() ext-real non negative Element of NAT

x is epsilon-transitive epsilon-connected ordinal natural V30() V31() V32() ext-real non negative Element of NAT

y is epsilon-transitive epsilon-connected ordinal natural V30() V31() V32() ext-real non negative Element of NAT

A /. x is Element of bool FT

A /. y is Element of bool FT

B is epsilon-transitive epsilon-connected ordinal natural V30() V31() V32() ext-real non negative set

x + B is epsilon-transitive epsilon-connected ordinal natural V30() V31() V32() ext-real non negative Element of NAT

x is epsilon-transitive epsilon-connected ordinal natural V30() V31() V32() ext-real non negative Element of NAT

x + x is epsilon-transitive epsilon-connected ordinal natural V30() V31() V32() ext-real non negative Element of NAT

(x + x) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V30() V31() V32() ext-real positive non negative Element of NAT

x + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V30() V31() V32() ext-real positive non negative Element of NAT

x + (x + 1) is non empty epsilon-transitive epsilon-connected ordinal natural V30() V31() V32() ext-real positive non negative Element of NAT

A /. (x + x) is Element of bool FT

A /. (x + (x + 1)) is Element of bool FT

x + 0 is epsilon-transitive epsilon-connected ordinal natural V30() V31() V32() ext-real non negative Element of NAT

A /. (x + 0) is Element of bool FT

FT is set

bool FT is non empty Element of K32(K32(FT))

K32(FT) is non empty set

K32(K32(FT)) is non empty set

A is V7() V10( NAT ) V11( bool FT) Function-like FinSequence-like FinSequence of bool FT

len A is epsilon-transitive epsilon-connected ordinal natural V30() V31() V32() ext-real non negative Element of NAT

x is epsilon-transitive epsilon-connected ordinal natural V30() V31() V32() ext-real non negative Element of NAT

y is epsilon-transitive epsilon-connected ordinal natural V30() V31() V32() ext-real non negative Element of NAT

A /. y is Element of bool FT

A /. x is Element of bool FT

B is epsilon-transitive epsilon-connected ordinal natural V30() V31() V32() ext-real non negative Element of NAT

A /. B is Element of bool FT

x is epsilon-transitive epsilon-connected ordinal natural V30() V31() V32() ext-real non negative Element of NAT

x + x is epsilon-transitive epsilon-connected ordinal natural V30() V31() V32() ext-real non negative Element of NAT

A /. (x + x) is Element of bool FT

(x + x) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V30() V31() V32() ext-real positive non negative Element of NAT

x + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V30() V31() V32() ext-real positive non negative Element of NAT

x + (x + 1) is non empty epsilon-transitive epsilon-connected ordinal natural V30() V31() V32() ext-real positive non negative Element of NAT

A /. (x + (x + 1)) is Element of bool FT

A /. ((x + x) + 1) is Element of bool FT

x + 0 is epsilon-transitive epsilon-connected ordinal natural V30() V31() V32() ext-real non negative Element of NAT

A /. (x + 0) is Element of bool FT

x is epsilon-transitive epsilon-connected ordinal natural V30() V31() V32() ext-real non negative set

x + x is epsilon-transitive epsilon-connected ordinal natural V30() V31() V32() ext-real non negative Element of NAT

x is epsilon-transitive epsilon-connected ordinal natural V30() V31() V32() ext-real non negative Element of NAT

x + x is epsilon-transitive epsilon-connected ordinal natural V30() V31() V32() ext-real non negative Element of NAT

F

K32(F

F

F

bool F

K32(K32(F

K33(NAT,(bool F

K32(K33(NAT,(bool F

FT is V7() V10( NAT ) V11( bool F

FT . 0 is Element of bool F

A is epsilon-transitive epsilon-connected ordinal natural V30() V31() V32() ext-real non negative Element of NAT

FT . A is Element of bool F

A + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V30() V31() V32() ext-real positive non negative Element of NAT

FT . (A + 1) is Element of bool F

F

A is epsilon-transitive epsilon-connected ordinal natural V30() V31() V32() ext-real non negative Element of NAT

FT . A is Element of bool F

A + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V30() V31() V32() ext-real positive non negative Element of NAT

FT . (A + 1) is Element of bool F

F

dom FT is Element of K32(NAT)

rng FT is Element of K32((bool F

K32((bool F

A is set

x is set

y is set

FT . y is set

x is set

FT . x is set

B is epsilon-transitive epsilon-connected ordinal natural V30() V31() V32() ext-real non negative Element of NAT

x is epsilon-transitive epsilon-connected ordinal natural V30() V31() V32() ext-real non negative Element of NAT

bool F

K32(F

K32(K32(F

A is set

FT .: NAT is Element of K32((bool F

x is epsilon-transitive epsilon-connected ordinal natural V30() V31() V32() ext-real non negative Element of NAT

FT . x is Element of bool F

A is set

FT .: NAT is Element of K32((bool F

x is epsilon-transitive epsilon-connected ordinal natural V30() V31() V32() ext-real non negative Element of NAT

FT . x is set

x is epsilon-transitive epsilon-connected ordinal natural V30() V31() V32() ext-real non negative set

FT . x is set

x + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V30() V31() V32() ext-real positive non negative Element of NAT

y is V7() V10( NAT ) V11( bool F

len y is epsilon-transitive epsilon-connected ordinal natural V30() V31() V32() ext-real non negative Element of NAT

dom y is Element of K32(NAT)

0 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V30() V31() V32() ext-real positive non negative Element of NAT

Seg (x + 1) is Element of K32(NAT)

y /. 1 is Element of bool F

y /. (len y) is Element of bool F

F

y . 1 is set

1 - 1 is V30() V31() V32() ext-real set

abs (1 - 1) is epsilon-transitive epsilon-connected ordinal natural V30() V31() V32() ext-real non negative Element of NAT

FT . (abs (1 - 1)) is Element of bool F

B is epsilon-transitive epsilon-connected ordinal natural V30() V31() V32() ext-real non negative Element of NAT

B + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V30() V31() V32() ext-real positive non negative Element of NAT

y /. (B + 1) is Element of bool F

y /. B is Element of bool F

F

y . B is set

B - 1 is V30() V31() V32() ext-real set

abs (B - 1) is epsilon-transitive epsilon-connected ordinal natural V30() V31() V32() ext-real non negative Element of NAT

FT . (abs (B - 1)) is Element of bool F

(B - 1) * 1 is V30() V31() V32() ext-real set

y . (B + 1) is set

(B + 1) - 1 is V30() V31() V32() ext-real set

abs ((B + 1) - 1) is epsilon-transitive epsilon-connected ordinal natural V30() V31() V32() ext-real non negative Element of NAT

FT . (abs ((B + 1) - 1)) is Element of bool F

(B - 1) + 1 is V30() V31() V32() ext-real set

abs ((B - 1) + 1) is epsilon-transitive epsilon-connected ordinal natural V30() V31() V32() ext-real non negative Element of NAT

FT . (abs ((B - 1) + 1)) is Element of bool F

abs 1 is epsilon-transitive epsilon-connected ordinal natural V30() V31() V32() ext-real non negative Element of NAT

(abs (B - 1)) + (abs 1) is epsilon-transitive epsilon-connected ordinal natural V30() V31() V32() ext-real non negative Element of NAT

FT . ((abs (B - 1)) + (abs 1)) is Element of bool F

(abs (B - 1)) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V30() V31() V32() ext-real positive non negative Element of NAT

FT . ((abs (B - 1)) + 1) is Element of bool F

F

FT . (x + 1) is Element of bool F

FT . x is Element of bool F

Seg (len y) is Element of K32(NAT)

y . (len y) is set

(x + 1) - 1 is V30() V31() V32() ext-real set

abs ((x + 1) - 1) is epsilon-transitive epsilon-connected ordinal natural V30() V31() V32() ext-real non negative Element of NAT

FT . (abs ((x + 1) - 1)) is Element of bool F

B is epsilon-transitive epsilon-connected ordinal natural V30() V31() V32() ext-real non negative Element of NAT

FT . B is Element of bool F

F

B is epsilon-transitive epsilon-connected ordinal natural V30() V31() V32() ext-real non negative Element of NAT

x is epsilon-transitive epsilon-connected ordinal natural V30() V31() V32() ext-real non negative Element of NAT

y /. B is Element of bool F

y /. x is Element of bool F

B - 1 is V30() V31() V32() ext-real set

y . B is set

abs (B - 1) is epsilon-transitive epsilon-connected ordinal natural V30() V31() V32() ext-real non negative Element of NAT

FT . (abs (B - 1)) is Element of bool F

x is epsilon-transitive epsilon-connected ordinal natural V30() V31() V32() ext-real non negative Element of NAT

FT . x is Element of bool F

y is epsilon-transitive epsilon-connected ordinal natural V30() V31() V32() ext-real non negative Element of NAT

y /. y is Element of bool F

y + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V30() V31() V32() ext-real positive non negative Element of NAT

y /. (y + 1) is Element of bool F

y - 1 is V30() V31() V32() ext-real set

y . (y + 1) is set

(y + 1) - 1 is V30() V31() V32() ext-real set

abs ((y + 1) - 1) is epsilon-transitive epsilon-connected ordinal natural V30() V31() V32() ext-real non negative Element of NAT

FT . (abs ((y + 1) - 1)) is Element of bool F

(y - 1) + 1 is V30() V31() V32() ext-real set

FT . ((y - 1) + 1) is set

y . y is set

abs (y - 1) is epsilon-transitive epsilon-connected ordinal natural V30() V31() V32() ext-real non negative Element of NAT

FT . (abs (y - 1)) is Element of bool F

FT . (y - 1) is set

B + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V30() V31() V32() ext-real positive non negative Element of NAT

y /. (B + 1) is Element of bool F

F

y is epsilon-transitive epsilon-connected ordinal natural V30() V31() V32() ext-real non negative Element of NAT

B + y is epsilon-transitive epsilon-connected ordinal natural V30() V31() V32() ext-real non negative Element of NAT

y /. (B + y) is Element of bool F

y + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V30() V31() V32() ext-real positive non negative Element of NAT

B + (y + 1) is non empty epsilon-transitive epsilon-connected ordinal natural V30() V31() V32() ext-real positive non negative Element of NAT

y /. (B + (y + 1)) is Element of bool F

(B + y) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V30() V31() V32() ext-real positive non negative Element of NAT

y /. ((B + y) + 1) is Element of bool F

y is epsilon-transitive epsilon-connected ordinal natural V30() V31() V32() ext-real non negative set

B + y is epsilon-transitive epsilon-connected ordinal natural V30() V31() V32() ext-real non negative Element of NAT

c

B + c

B + 0 is epsilon-transitive epsilon-connected ordinal natural V30() V31() V32() ext-real non negative Element of NAT

y /. (B + 0) is Element of bool F

y /. (x + 1) is Element of bool F

y . (x + 1) is set

(x + 1) - 1 is V30() V31() V32() ext-real set

abs ((x + 1) - 1) is epsilon-transitive epsilon-connected ordinal natural V30() V31() V32() ext-real non negative Element of NAT

FT . (abs ((x + 1) - 1)) is Element of bool F

x + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V30() V31() V32() ext-real positive non negative Element of NAT

the non empty set is non empty set

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

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

the V7() V10( the non empty set ) V11( the non empty set ) Element of K32(K33( the non empty set , the non empty set )) is V7() V10( the non empty set ) V11( the non empty set ) Element of K32(K33( the non empty set , the non empty set ))

RelStr(# the non empty set , the V7() V10( the non empty set ) V11( the non empty set ) Element of K32(K33( the non empty set , the non empty set )) #) is strict RelStr

the carrier of RelStr(# the non empty set , the V7() V10( the non empty set ) V11( the non empty set ) Element of K32(K33( the non empty set , the non empty set )) #) is set

FT is RelStr

the carrier of FT is set

the InternalRel of FT is V7() V10( the carrier of FT) V11( the carrier of FT) Element of K32(K33( the carrier of FT, the carrier of FT))

K33( the carrier of FT, the carrier of FT) is set

K32(K33( the carrier of FT, the carrier of FT)) is non empty set

A is Element of the carrier of FT

Class ( the InternalRel of FT,A) is Element of K32( the carrier of FT)

K32( the carrier of FT) is non empty set

{A} is non empty finite set

the InternalRel of FT .: {A} is set

FT is set

{FT} is non empty finite set

K32({FT}) is non empty finite V50() set

A is finite Element of K32({FT})

FT .--> A is V7() V10({FT}) V11(K32({FT})) Function-like one-to-one finite set

{FT} --> A is non empty V7() V10({FT}) V11(K32({FT})) V11({A}) Function-like constant total quasi_total finite Element of K32(K33({FT},{A}))

{A} is non empty finite V50() set

K33({FT},{A}) is non empty finite set

K32(K33({FT},{A})) is non empty finite V50() set

bool {FT} is non empty finite V50() Element of K32(K32({FT}))

K32(K32({FT})) is non empty finite V50() set

K33({FT},(bool {FT})) is non empty finite set

K32(K33({FT},(bool {FT}))) is non empty finite V50() set

dom (FT .--> A) is finite Element of K32({FT})

rng (FT .--> A) is finite V50() Element of K32(K32({FT}))

{A} is non empty finite V50() Element of K32(K32({FT}))

x is V7() V10({FT}) V11( bool {FT}) finite Element of K32(K33({FT},(bool {FT})))

FT is set

[FT,FT] is set

{FT,FT} is non empty finite set

{FT} is non empty finite set

{{FT,FT},{FT}} is non empty finite V50() set

{[FT,FT]} is non empty finite set

K33({FT},{FT}) is non empty finite set

K32(K33({FT},{FT})) is non empty finite V50() set

{0} is non empty finite V50() Element of K32(NAT)

(0) is V7() V10({0}) V11({0}) finite Element of K32(K33({0},{0}))

{0} is non empty finite V50() set

K33({0},{0}) is non empty finite set

K32(K33({0},{0})) is non empty finite V50() set

[0,0] is set

{0,0} is non empty finite V50() set

{{0,0},{0}} is non empty finite V50() set

{[0,0]} is non empty finite set

RelStr(# {0},(0) #) is strict RelStr

() is strict RelStr

FT is non empty RelStr

the carrier of FT is non empty set

A is Element of the carrier of FT

(FT,A) is Element of K32( the carrier of FT)

K32( the carrier of FT) is non empty set

the InternalRel of FT is V7() V10( the carrier of FT) V11( the carrier of FT) Element of K32(K33( the carrier of FT, the carrier of FT))

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

K32(K33( the carrier of FT, the carrier of FT)) is non empty set

Class ( the InternalRel of FT,A) is Element of K32( the carrier of FT)

{A} is non empty finite set

the InternalRel of FT .: {A} is set

[A,A] is Element of K33( the carrier of FT, the carrier of FT)

{A,A} is non empty finite set

{{A,A},{A}} is non empty finite V50() set

A is set

[A,A] is set

{A,A} is non empty finite set

{A} is non empty finite set

{{A,A},{A}} is non empty finite V50() set

the InternalRel of FT is V7() V10( the carrier of FT) V11( the carrier of FT) Element of K32(K33( the carrier of FT, the carrier of FT))

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

K32(K33( the carrier of FT, the carrier of FT)) is non empty set

x is Element of the carrier of FT

(FT,x) is Element of K32( the carrier of FT)

K32( the carrier of FT) is non empty set

Class ( the InternalRel of FT,x) is Element of K32( the carrier of FT)

{x} is non empty finite set

the InternalRel of FT .: {x} is set

the carrier of () is non empty set

FT is Element of the carrier of ()

((),FT) is Element of K32( the carrier of ())

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

the InternalRel of () is V7() V10( the carrier of ()) V11( the carrier of ()) Element of K32(K33( the carrier of (), the carrier of ()))

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

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

Class ( the InternalRel of (),FT) is Element of K32( the carrier of ())

{FT} is non empty finite set

the InternalRel of () .: {FT} is set

[0,0] is Element of K33(NAT,NAT)

K33(NAT,NAT) is non empty set

FT is non empty reflexive RelStr

the carrier of FT is non empty set

{ (FT,b

A is set

union { (FT,b

x is Element of the carrier of FT

(FT,x) is Element of K32( the carrier of FT)

K32( the carrier of FT) is non empty set

the InternalRel of FT is V7() V10( the carrier of FT) V11( the carrier of FT) Element of K32(K33( the carrier of FT, the carrier of FT))

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

K32(K33( the carrier of FT, the carrier of FT)) is non empty set

Class ( the InternalRel of FT,x) is Element of K32( the carrier of FT)

{x} is non empty finite set

the InternalRel of FT .: {x} is set

FT is non empty RelStr

the carrier of FT is non empty set

K32( the carrier of FT) is non empty set

A is Element of K32( the carrier of FT)

A ` is Element of K32( the carrier of FT)

the carrier of FT \ A is set

{ b

{ b

FT is non empty RelStr

the carrier of FT is non empty set

K32( the carrier of FT) is non empty set

A is Element of the carrier of FT

(FT,A) is Element of K32( the carrier of FT)

the InternalRel of FT is V7() V10( the carrier of FT) V11( the carrier of FT) Element of K32(K33( the carrier of FT, the carrier of FT))

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

K32(K33( the carrier of FT, the carrier of FT)) is non empty set

Class ( the InternalRel of FT,A) is Element of K32( the carrier of FT)

{A} is non empty finite set

the InternalRel of FT .: {A} is set

x is Element of K32( the carrier of FT)

(FT,x) is Element of K32( the carrier of FT)

x ` is Element of K32( the carrier of FT)

the carrier of FT \ x is set

{ b

y is Element of the carrier of FT

(FT,y) is Element of K32( the carrier of FT)

Class ( the InternalRel of FT,y) is Element of K32( the carrier of FT)

{y} is non empty finite set

the InternalRel of FT .: {y} is set

FT is non empty RelStr

the carrier of FT is non empty set

K32( the carrier of FT) is non empty set

A is Element of K32( the carrier of FT)

(FT,A) is Element of K32( the carrier of FT)

A ` is Element of K32( the carrier of FT)

the carrier of FT \ A is set

{ b

A /\ (FT,A) is Element of K32( the carrier of FT)

(A `) /\ (FT,A) is Element of K32( the carrier of FT)

FT is non empty RelStr

the carrier of FT is non empty set

K32( the carrier of FT) is non empty set

A is Element of K32( the carrier of FT)

(FT,A) is Element of K32( the carrier of FT)

A ` is Element of K32( the carrier of FT)

the carrier of FT \ A is set

{ b

(FT,A) is Element of K32( the carrier of FT)

A /\ (FT,A) is Element of K32( the carrier of FT)

(FT,A) is Element of K32( the carrier of FT)

(A `) /\ (FT,A) is Element of K32( the carrier of FT)

(FT,A) \/ (FT,A) is Element of K32( the carrier of FT)

x is set

[#] the carrier of FT is non empty non proper Element of K32( the carrier of FT)

([#] the carrier of FT) /\ (FT,A) is Element of K32( the carrier of FT)

A \/ (A `) is Element of K32( the carrier of FT)

(A \/ (A `)) /\ (FT,A) is Element of K32( the carrier of FT)

A \/ (A `) is Element of K32( the carrier of FT)

(A \/ (A `)) /\ (FT,A) is Element of K32( the carrier of FT)

[#] the carrier of FT is non empty non proper Element of K32( the carrier of FT)

([#] the carrier of FT) /\ (FT,A) is Element of K32( the carrier of FT)

FT is non empty RelStr

the carrier of FT is non empty set

K32( the carrier of FT) is non empty set

A is Element of K32( the carrier of FT)

{ b

{ b

{ b

{ b

{ b

{ b

FT is non empty RelStr

the carrier of FT is non empty set

K32( the carrier of FT) is non empty set

A is Element of K32( the carrier of FT)

(FT,A) is Element of K32( the carrier of FT)

{ b

A \ (FT,A) is Element of K32( the carrier of FT)

{ b

( b

{ b

FT is non empty RelStr

the carrier of FT is non empty set

K32( the carrier of FT) is non empty set

A is Element of the carrier of FT

(FT,A) is Element of K32( the carrier of FT)

the InternalRel of FT is V7() V10( the carrier of FT) V11( the carrier of FT) Element of K32(K33( the carrier of FT, the carrier of FT))

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

K32(K33( the carrier of FT, the carrier of FT)) is non empty set

Class ( the InternalRel of FT,A) is Element of K32( the carrier of FT)

{A} is non empty finite set

the InternalRel of FT .: {A} is set

x is Element of K32( the carrier of FT)

(FT,x) is Element of K32( the carrier of FT)

{ b

y is Element of the carrier of FT

(FT,y) is Element of K32( the carrier of FT)

Class ( the InternalRel of FT,y) is Element of K32( the carrier of FT)

{y} is non empty finite set

the InternalRel of FT .: {y} is set

FT is non empty RelStr

the carrier of FT is non empty set

K32( the carrier of FT) is non empty set

A is Element of the carrier of FT

(FT,A) is Element of K32( the carrier of FT)

the InternalRel of FT is V7() V10( the carrier of FT) V11( the carrier of FT) Element of K32(K33( the carrier of FT, the carrier of FT))

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

K32(K33( the carrier of FT, the carrier of FT)) is non empty set

Class ( the InternalRel of FT,A) is Element of K32( the carrier of FT)

{A} is non empty finite set

the InternalRel of FT .: {A} is set

x is Element of K32( the carrier of FT)

(FT,x) is Element of K32( the carrier of FT)

{ b

y is Element of the carrier of FT

(FT,y) is Element of K32( the carrier of FT)

Class ( the InternalRel of FT,y) is Element of K32( the carrier of FT)

{y} is non empty finite set

the InternalRel of FT .: {y} is set

FT is non empty RelStr

the carrier of FT is non empty set

K32( the carrier of FT) is non empty set

A is Element of the carrier of FT

(FT,A) is Element of K32( the carrier of FT)

the InternalRel of FT is V7() V10( the carrier of FT) V11( the carrier of FT) Element of K32(K33( the carrier of FT, the carrier of FT))

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

K32(K33( the carrier of FT, the carrier of FT)) is non empty set

Class ( the InternalRel of FT,A) is Element of K32( the carrier of FT)

{A} is non empty finite set

the InternalRel of FT .: {A} is set

{A} is non empty finite Element of K32( the carrier of FT)

(FT,A) \ {A} is Element of K32( the carrier of FT)

x is Element of K32( the carrier of FT)

(FT,x) is Element of K32( the carrier of FT)

{ b

y is Element of the carrier of FT

(FT,y) is Element of K32( the carrier of FT)

Class ( the InternalRel of FT,y) is Element of K32( the carrier of FT)

{y} is non empty finite set

the InternalRel of FT .: {y} is set

{y} is non empty finite Element of K32( the carrier of FT)

(FT,y) \ {y} is Element of K32( the carrier of FT)

FT is non empty RelStr

the carrier of FT is non empty set

K32( the carrier of FT) is non empty set

A is Element of the carrier of FT

(FT,A) is Element of K32( the carrier of FT)

the InternalRel of FT is V7() V10( the carrier of FT) V11( the carrier of FT) Element of K32(K33( the carrier of FT, the carrier of FT))

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

K32(K33( the carrier of FT, the carrier of FT)) is non empty set

Class ( the InternalRel of FT,A) is Element of K32( the carrier of FT)

{A} is non empty finite set

the InternalRel of FT .: {A} is set

{A} is non empty finite Element of K32( the carrier of FT)

(FT,A) \ {A} is Element of K32( the carrier of FT)

x is Element of K32( the carrier of FT)

(FT,x) is Element of K32( the carrier of FT)

(FT,x) is Element of K32( the carrier of FT)

{ b

x \ (FT,x) is Element of K32( the carrier of FT)

FT is non empty RelStr

the carrier of FT is non empty set

K32( the carrier of FT) is non empty set

A is Element of the carrier of FT

x is Element of K32( the carrier of FT)

(FT,x) is Element of K32( the carrier of FT)

{ b

( b

y is Element of the carrier of FT

B is Element of the carrier of FT

(FT,B) is Element of K32( the carrier of FT)

the InternalRel of FT is V7() V10( the carrier of FT) V11( the carrier of FT) Element of K32(K33( the carrier of FT, the carrier of FT))

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

K32(K33( the carrier of FT, the carrier of FT)) is non empty set

Class ( the InternalRel of FT,B) is Element of K32( the carrier of FT)

{B} is non empty finite set

the InternalRel of FT .: {B} is set

y is Element of the carrier of FT

(FT,y) is Element of K32( the carrier of FT)

the InternalRel of FT is V7() V10( the carrier of FT) V11( the carrier of FT) Element of K32(K33( the carrier of FT, the carrier of FT))

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

K32(K33( the carrier of FT, the carrier of FT)) is non empty set

Class ( the InternalRel of FT,y) is Element of K32( the carrier of FT)

{y} is non empty finite set

the InternalRel of FT .: {y} is set

FT is non empty RelStr

the carrier of FT is non empty set

K32( the carrier of FT) is non empty set

A is Element of K32( the carrier of FT)

(FT,A) is Element of K32( the carrier of FT)

{ b

(FT,A) is Element of K32( the carrier of FT)

{ b

( b

x is set

y is Element of the carrier of FT

(FT,y) is Element of K32( the carrier of FT)

the InternalRel of FT is V7() V10( the carrier of FT) V11( the carrier of FT) Element of K32(K33( the carrier of FT, the carrier of FT))

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

K32(K33( the carrier of FT, the carrier of FT)) is non empty set

Class ( the InternalRel of FT,y) is Element of K32( the carrier of FT)

{y} is non empty finite set

the InternalRel of FT .: {y} is set

(FT,y) /\ A is Element of K32( the carrier of FT)

B is set

x is Element of the carrier of FT

(FT,x) is Element of K32( the carrier of FT)

Class ( the InternalRel of FT,x) is Element of K32( the carrier of FT)

{x} is non empty finite set

the InternalRel of FT .: {x} is set

x is set

y is Element of the carrier of FT

B is Element of the carrier of FT

(FT,B) is Element of K32( the carrier of FT)

the InternalRel of FT is V7() V10( the carrier of FT) V11( the carrier of FT) Element of K32(K33( the carrier of FT, the carrier of FT))

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

K32(K33( the carrier of FT, the carrier of FT)) is non empty set

Class ( the InternalRel of FT,B) is Element of K32( the carrier of FT)

{B} is non empty finite set

the InternalRel of FT .: {B} is set

(FT,y) is Element of K32( the carrier of FT)

Class ( the InternalRel of FT,y) is Element of K32( the carrier of FT)

{y} is non empty finite set

the InternalRel of FT .: {y} is set

x is Element of the carrier of FT

A is Element of the carrier of FT

(FT,A) is Element of K32( the carrier of FT)

the InternalRel of FT is V7() V10( the carrier of FT) V11( the carrier of FT) Element of K32(K33( the carrier of FT, the carrier of FT))

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

K32(K33( the carrier of FT, the carrier of FT)) is non empty set

Class ( the InternalRel of FT,A) is Element of K32( the carrier of FT)

{A} is non empty finite set

the InternalRel of FT .: {A} is set

(FT,x) is Element of K32( the carrier of FT)

Class ( the InternalRel of FT,x) is Element of K32( the carrier of FT)

{x} is non empty finite set

the InternalRel of FT .: {x} is set

{x} is non empty finite Element of K32( the carrier of FT)

(FT,{x}) is Element of K32( the carrier of FT)

{ b

(FT,{x}) is Element of K32( the carrier of FT)

{ b

( b

y is Element of the carrier of FT

(FT,y) is Element of K32( the carrier of FT)

Class ( the InternalRel of FT,y) is Element of K32( the carrier of FT)

{y} is non empty finite set

the InternalRel of FT .: {y} is set

FT is non empty RelStr

the carrier of FT is non empty set

K32( the carrier of FT) is non empty set

FT is non empty RelStr

the carrier of FT is non empty set

K32( the carrier of FT) is non empty set

A is Element of K32( the carrier of FT)

{ b

meet { b

bool the carrier of FT is non empty Element of K32(K32( the carrier of FT))

K32(K32( the carrier of FT)) is non empty set

y is set

B is Element of K32( the carrier of FT)

y is Element of K32(K32( the carrier of FT))

meet y is Element of K32( the carrier of FT)

{ b

union { b

bool the carrier of FT is non empty Element of K32(K32( the carrier of FT))

K32(K32( the carrier of FT)) is non empty set

y is set

B is Element of K32( the carrier of FT)

y is Element of K32(K32( the carrier of FT))

union y is Element of K32( the carrier of FT)

FT is non empty reflexive RelStr

the carrier of FT is non empty set

K32( the carrier of FT) is non empty set

A is Element of K32( the carrier of FT)

(FT,A) is Element of K32( the carrier of FT)

{ b

x is set

y is Element of the carrier of FT

(FT,y) is Element of K32( the carrier of FT)

the InternalRel of FT is V7() V10( the carrier of FT) V11( the carrier of FT) Element of K32(K33( the carrier of FT, the carrier of FT))

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

K32(K33( the carrier of FT, the carrier of FT)) is non empty set

Class ( the InternalRel of FT,y) is Element of K32( the carrier of FT)

{y} is non empty finite set

the InternalRel of FT .: {y} is set

FT is non empty RelStr

the carrier of FT is non empty set

K32( the carrier of FT) is non empty set

A is Element of K32( the carrier of FT)

x is Element of K32( the carrier of FT)

(FT,A) is Element of K32( the carrier of FT)

{ b

(FT,x) is Element of K32( the carrier of FT)

{ b

y is set

B is Element of the carrier of FT

(FT,B) is Element of K32( the carrier of FT)

the InternalRel of FT is V7() V10( the carrier of FT) V11( the carrier of FT) Element of K32(K33( the carrier of FT, the carrier of FT))

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

K32(K33( the carrier of FT, the carrier of FT)) is non empty set

Class ( the InternalRel of FT,B) is Element of K32( the carrier of FT)

{B} is non empty finite set

the InternalRel of FT .: {B} is set

x is set

FT is non empty finite reflexive RelStr

the carrier of FT is non empty finite set

K32( the carrier of FT) is non empty finite V50() set

bool the carrier of FT is non empty finite V50() Element of K32(K32( the carrier of FT))

K32(K32( the carrier of FT)) is non empty finite V50() set

A is finite Element of K32( the carrier of FT)

x is Element of the carrier of FT

{x} is non empty finite Element of K32( the carrier of FT)

y is finite Element of K32( the carrier of FT)

(FT,y) is finite Element of K32( the carrier of FT)

{ b

(FT,y) /\ A is finite Element of K32( the carrier of FT)

y is V7() V10( NAT ) V11( bool the carrier of FT) Function-like FinSequence-like FinSequence of bool the carrier of FT

len y is epsilon-transitive epsilon-connected ordinal natural V30() V31() V32() ext-real non negative Element of NAT

y /. 1 is finite Element of bool the carrier of FT

y /. (len y) is finite Element of bool the carrier of FT

(FT,(y /. (len y))) is finite Element of K32( the carrier of FT)

{ b

(FT,(y /. (len y))) /\ A is finite Element of K32( the carrier of FT)

B is epsilon-transitive epsilon-connected ordinal natural V30() V31() V32() ext-real non negative set

B + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V30() V31() V32() ext-real positive non negative Element of NAT

A \ (y /. (len y)) is finite Element of K32( the carrier of FT)

y is epsilon-transitive epsilon-connected ordinal natural V30() V31() V32() ext-real non negative Element of NAT

y + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V30() V31() V32() ext-real positive non negative Element of NAT

y /. (y + 1) is finite Element of bool the carrier of FT

(y + 1) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V30() V31() V32() ext-real positive non negative Element of NAT

y /. ((y + 1) + 1) is finite Element of bool the carrier of FT

0 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V30() V31() V32() ext-real positive non negative Element of NAT

y /. (0 + 1) is finite Element of bool the carrier of FT

y is epsilon-transitive epsilon-connected ordinal natural V30() V31() V32() ext-real non negative Element of NAT

c

c

y /. (c

y /. c

(FT,(y /. c

{ b

(FT,(y /. c

(FT,(y /. (len y))) /\ (A \ (y /. (len y))) is finite Element of K32( the carrier of FT)

A /\ (A \ (y /. (len y))) is finite Element of K32( the carrier of FT)

(FT,(y /. (len y))) /\ (A /\ (A \ (y /. (len y)))) is finite Element of K32( the carrier of FT)

(y /. (len y)) /\ (A \ (y /. (len y))) is finite Element of K32( the carrier of FT)

(y /. (len y)) \/ (A \ (y /. (len y))) is finite Element of K32( the carrier of FT)

(y /. (len y)) \/ A is finite Element of K32( the carrier of FT)

x is finite Element of K32( the carrier of FT)

y is finite Element of K32( the carrier of FT)

x \/ y is finite Element of K32( the carrier of FT)

(FT,x) is finite Element of K32( the carrier of FT)

{ b

the Element of x is Element of x

{ the Element of x} is non empty finite set

x is V7() V10( NAT ) V11( bool the carrier of FT) Function-like FinSequence-like FinSequence of bool the carrier of FT

len x is epsilon-transitive epsilon-connected ordinal natural V30() V31() V32() ext-real non negative Element of NAT

x /. 1 is finite Element of bool the carrier of FT

x /. (len x) is finite Element of bool the carrier of FT

x is epsilon-transitive epsilon-connected ordinal natural V30() V31() V32() ext-real non negative set

x + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V30() V31() V32() ext-real positive non negative Element of NAT

(FT,x) /\ y is finite Element of K32( the carrier of FT)

(FT,x) /\ A is finite Element of K32( the carrier of FT)

(FT,x) /\ x is finite Element of K32( the carrier of FT)

((FT,x) /\ x) \/ {} is finite set

y is epsilon-transitive epsilon-connected ordinal natural V30() V31() V32() ext-real non negative Element of NAT

y + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V30() V31() V32() ext-real positive non negative Element of NAT

x /. (y + 1) is finite Element of bool the carrier of FT

(y + 1) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V30() V31() V32() ext-real positive non negative Element of NAT

x /. ((y + 1) + 1) is finite Element of bool the carrier of FT

(FT,(x /. (y + 1))) is finite Element of K32( the carrier of FT)

{ b

(FT,(x /. (y + 1))) /\ A is finite Element of K32( the carrier of FT)

0 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V30() V31() V32() ext-real positive non negative Element of NAT

x /. (0 + 1) is finite Element of bool the carrier of FT

y is epsilon-transitive epsilon-connected ordinal natural V30() V31() V32() ext-real non negative Element of NAT

x /\ y is finite Element of K32( the carrier of FT)

FT is non empty RelStr

the carrier of FT is non empty set

K32( the carrier of FT) is non empty set

A is Element of K32( the carrier of FT)

A ` is Element of K32( the carrier of FT)

the carrier of FT \ A is set

(FT,(A `)) is Element of K32( the carrier of FT)

{ b

(FT,(A `)) ` is Element of K32( the carrier of FT)

the carrier of FT \ (FT,(A `)) is set

(FT,A) is Element of K32( the carrier of FT)

{ b

x is set

y is Element of the carrier of FT

(FT,y) is Element of K32( the carrier of FT)

the InternalRel of FT is V7() V10( the carrier of FT) V11( the carrier of FT) Element of K32(K33( the carrier of FT, the carrier of FT))

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

K32(K33( the carrier of FT, the carrier of FT)) is non empty set

Class ( the InternalRel of FT,y) is Element of K32( the carrier of FT)

{y} is non empty finite set

the InternalRel of FT .: {y} is set

B is set

y is Element of the carrier of FT

(FT,y) is Element of K32( the carrier of FT)

the InternalRel of FT is V7() V10( the carrier of FT) V11( the carrier of FT) Element of K32(K33( the carrier of FT, the carrier of FT))

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

K32(K33( the carrier of FT, the carrier of FT)) is non empty set

Class ( the InternalRel of FT,y) is Element of K32( the carrier of FT)

{y} is non empty finite set

the InternalRel of FT .: {y} is set

B is set

FT is non empty RelStr

the carrier of FT is non empty set

K32( the carrier of FT) is non empty set

A is Element of K32( the carrier of FT)

A ` is Element of K32( the carrier of FT)

the carrier of FT \ A is set

(FT,(A `)) is Element of K32( the carrier of FT)

{ b

(FT,(A `)) ` is Element of K32( the carrier of FT)

the carrier of FT \ (FT,(A `)) is set

(FT,A) is Element of K32( the carrier of FT)

{ b

x is set

y is Element of the carrier of FT

(FT,y) is Element of K32( the carrier of FT)

the InternalRel of FT is V7() V10( the carrier of FT) V11( the carrier of FT) Element of K32(K33( the carrier of FT, the carrier of FT))

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

K32(K33( the carrier of FT, the carrier of FT)) is non empty set

Class ( the InternalRel of FT,y) is Element of K32( the carrier of FT)

{y} is non empty finite set

the InternalRel of FT .: {y} is set

(FT,y) /\ (A `) is Element of K32( the carrier of FT)

(FT,y) \ A is Element of K32( the carrier of FT)

y is Element of the carrier of FT

(FT,y) is Element of K32( the carrier of FT)

the InternalRel of FT is V7() V10( the carrier of FT) V11( the carrier of FT) Element of K32(K33( the carrier of FT, the carrier of FT))

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

K32(K33( the carrier of FT, the carrier of FT)) is non empty set

Class ( the InternalRel of FT,y) is Element of K32( the carrier of FT)

{y} is non empty finite set

the InternalRel of FT .: {y} is set

(FT,y) \ A is Element of K32( the carrier of FT)

(FT,y) /\ (A `) is Element of K32( the carrier of FT)

FT is non empty RelStr

the carrier of FT is non empty set

K32( the carrier of FT) is non empty set

A is Element of K32( the carrier of FT)

(FT,A) is Element of K32( the carrier of FT)

A ` is Element of K32( the carrier of FT)

the carrier of FT \ A is set

{ b

(FT,A) is Element of K32( the carrier of FT)

{ b

(FT,(A `)) is Element of K32( the carrier of FT)

{ b

(FT,A) /\ (FT,(A `)) is Element of K32( the carrier of FT)

x is set

y is Element of the carrier of FT

(FT,y) is Element of K32( the carrier of FT)

the InternalRel of FT is V7() V10( the carrier of FT) V11( the carrier of FT) Element of K32(K33( the carrier of FT, the carrier of FT))

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

K32(K33( the carrier of FT, the carrier of FT)) is non empty set

Class ( the InternalRel of FT,y) is Element of K32( the carrier of FT)

{y} is non empty finite set

the InternalRel of FT .: {y} is set

y is Element of the carrier of FT

(FT,y) is Element of K32( the carrier of FT)

the InternalRel of FT is V7() V10( the carrier of FT) V11( the carrier of FT) Element of K32(K33( the carrier of FT, the carrier of FT))

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

K32(K33( the carrier of FT, the carrier of FT)) is non empty set

Class ( the InternalRel of FT,y) is Element of K32( the carrier of FT)

{y} is non empty finite set

the InternalRel of FT .: {y} is set

FT is non empty RelStr

the carrier of FT is non empty set

K32( the carrier of FT) is non empty set

A is Element of K32( the carrier of FT)

A ` is Element of K32( the carrier of FT)

the carrier of FT \ A is set

(FT,(A `)) is Element of K32( the carrier of FT)

(A `) ` is Element of K32( the carrier of FT)

the carrier of FT \ (A `) is set

{ b

(FT,A) is Element of K32( the carrier of FT)

{ b

x is set

y is Element of the carrier of FT

(FT,y) is Element of K32( the carrier of FT)

the InternalRel of FT is V7() V10( the carrier of FT) V11( the carrier of FT) Element of K32(K33( the carrier of FT, the carrier of FT))

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

K32(K33( the carrier of FT, the carrier of FT)) is non empty set

Class ( the InternalRel of FT,y) is Element of K32( the carrier of FT)

{y} is non empty finite set

the InternalRel of FT .: {y} is set

y is Element of the carrier of FT

(FT,y) is Element of K32( the carrier of FT)

the InternalRel of FT is V7() V10( the carrier of FT) V11( the carrier of FT) Element of K32(K33( the carrier of FT, the carrier of FT))

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

K32(K33( the carrier of FT, the carrier of FT)) is non empty set

Class ( the InternalRel of FT,y) is Element of K32( the carrier of FT)

{y} is non empty finite set

the InternalRel of FT .: {y} is set

FT is non empty RelStr

the carrier of FT is non empty set

K32( the carrier of FT) is non empty set

A is Element of the carrier of FT

{A} is non empty finite Element of K32( the carrier of FT)

x is Element of K32( the carrier of FT)

(FT,x) is Element of K32( the carrier of FT)

{ b

x \ {A} is Element of K32( the carrier of FT)

(FT,(x \ {A})) is Element of K32( the carrier of FT)

{ b

(FT,A) is Element of K32( the carrier of FT)

the InternalRel of FT is V7() V10( the carrier of FT) V11( the carrier of FT) Element of K32(K33( the carrier of FT, the carrier of FT))

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

K32(K33( the carrier of FT, the carrier of FT)) is non empty set

Class ( the InternalRel of FT,A) is Element of K32( the carrier of FT)

{A} is non empty finite set

the InternalRel of FT .: {A} is set

(FT,A) \ {A} is Element of K32( the carrier of FT)

x /\ ((FT,A) \ {A}) is Element of K32( the carrier of FT)

x /\ (FT,A) is Element of K32( the carrier of FT)

(x /\ (FT,A)) \ {A} is Element of K32( the carrier of FT)

(FT,A) /\ x is Element of K32( the carrier of FT)

((FT,A) /\ x) \ {A} is Element of K32( the carrier of FT)

(FT,A) /\ (x \ {A}) is Element of K32( the carrier of FT)

FT is non empty RelStr

the carrier of FT is non empty set

K32( the carrier of FT) is non empty set

A is Element of K32( the carrier of FT)

(FT,A) is Element of K32( the carrier of FT)

{ b

card A is cardinal set

x is Element of the carrier of FT

{x} is non empty finite Element of K32( the carrier of FT)

A \ {x} is Element of K32( the carrier of FT)

card {x} is epsilon-transitive epsilon-connected ordinal natural V30() V31() V32() ext-real non negative Element of omega

K32(A) is non empty set

(A \ {x}) \/ {x} is non empty Element of K32( the carrier of FT)

(FT,x) is Element of K32( the carrier of FT)

the InternalRel of FT is V7() V10( the carrier of FT) V11( the carrier of FT) Element of K32(K33( the carrier of FT, the carrier of FT))

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

K32(K33( the carrier of FT, the carrier of FT)) is non empty set

Class ( the InternalRel of FT,x) is Element of K32( the carrier of FT)

{x} is non empty finite set

the InternalRel of FT .: {x} is set

(FT,x) \ {x} is Element of K32( the carrier of FT)

(FT,(A \ {x})) is Element of K32( the carrier of FT)

{ b

x is set

x is Element of the carrier of FT

(FT,x) is Element of K32( the carrier of FT)

Class ( the InternalRel of FT,x) is Element of K32( the carrier of FT)

{x} is non empty finite set

the InternalRel of FT .: {x} is set

y is set

{x} is non empty finite Element of K32( the carrier of FT)

(FT,x) \ {x} is Element of K32( the carrier of FT)

((FT,x) \ {x}) /\ (A \ {x}) is Element of K32( the carrier of FT)

((FT,x) \ {x}) /\ A is Element of K32( the carrier of FT)

c

FT is non empty reflexive RelStr

the carrier of FT is non empty set

K32( the carrier of FT) is non empty set

A is Element of K32( the carrier of FT)

(FT,A) is Element of K32( the carrier of FT)

{ b

x is set

y is Element of the carrier of FT

(FT,y) is Element of K32( the carrier of FT)

the InternalRel of FT is V7() V10( the carrier of FT) V11( the carrier of FT) Element of K32(K33( the carrier of FT, the carrier of FT))

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

K32(K33( the carrier of FT, the carrier of FT)) is non empty set

Class ( the InternalRel of FT,y) is Element of K32( the carrier of FT)

{y} is non empty finite set

the InternalRel of FT .: {y} is set

FT is non empty RelStr

the carrier of FT is non empty set

K32( the carrier of FT) is non empty set

A is Element of K32( the carrier of FT)

A ` is Element of K32( the carrier of FT)

the carrier of FT \ A is set

(FT,A) is Element of K32( the carrier of FT)

{ b

(FT,(A `)) is Element of K32( the carrier of FT)

{ b

(FT,(A `)) ` is Element of K32( the carrier of FT)

the carrier of FT \ (FT,(A `)) is set

FT is non empty RelStr

the carrier of FT is non empty set

K32( the carrier of FT) is non empty set

A is Element of K32( the carrier of FT)

A ` is Element of K32( the carrier of FT)

the carrier of FT \ A is set

(FT,A) is Element of K32( the carrier of FT)

{ b

(FT,(A `)) is Element of K32( the carrier of FT)

{ b

(FT,(A `)) ` is Element of K32( the carrier of FT)

the carrier of FT \ (FT,(A `)) is set