:: FIN_TOPO semantic presentation

REAL is set

K32(REAL) is non empty set

K32(omega) is non empty set
K32(NAT) is non empty set

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

A /. x is Element of bool FT
A /. y 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 + (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

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

A /. y is Element of bool FT
A /. x is Element of bool FT

A /. B is Element of bool FT

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 + (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

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

F1() is non empty set
K32(F1()) is non empty set
F2() is Element of K32(F1())
F3() is Element of K32(F1())
bool F1() is non empty Element of K32(K32(F1()))
K32(K32(F1())) is non empty set
K33(NAT,(bool F1())) is non empty set
K32(K33(NAT,(bool F1()))) is non empty set
FT is V7() V10( NAT ) V11( bool F1()) Function-like quasi_total Element of K32(K33(NAT,(bool F1())))
FT . 0 is Element of bool F1()

FT . A is Element of bool F1()

FT . (A + 1) is Element of bool F1()
F4((FT . A)) is Element of K32(F1())

FT . A is Element of bool F1()

FT . (A + 1) is Element of bool F1()
F4((FT . A)) is Element of K32(F1())
dom FT is Element of K32(NAT)
rng FT is Element of K32((bool F1()))
K32((bool F1())) is non empty set
A is set
x is set
y is set
FT . y is set
x is set
FT . x is set

bool F2() is non empty Element of K32(K32(F2()))
K32(F2()) is non empty set
K32(K32(F2())) is non empty set
A is set
FT .: NAT is Element of K32((bool F1()))

FT . x is Element of bool F1()
A is set
FT .: NAT is Element of K32((bool F1()))

FT . x is set

FT . x is set

y is V7() V10( NAT ) V11( bool F1()) Function-like FinSequence-like FinSequence of bool F1()

dom y is Element of K32(NAT)

Seg (x + 1) is Element of K32(NAT)
y /. 1 is Element of bool F1()
y /. (len y) is Element of bool F1()
F4((y /. (len y))) is Element of K32(F1())
y . 1 is set
1 - 1 is V30() V31() V32() ext-real set

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

y /. (B + 1) is Element of bool F1()
y /. B is Element of bool F1()
F4((y /. B)) is Element of K32(F1())
y . B is set
B - 1 is V30() V31() V32() ext-real set

FT . (abs (B - 1)) is Element of bool F1()
(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 F1()
(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 F1()

(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 F1()
(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 F1()
F4((FT . (abs (B - 1)))) is Element of K32(F1())
FT . (x + 1) is Element of bool F1()
FT . x is Element of bool F1()
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 F1()

FT . B is Element of bool F1()
F4((FT . B)) is Element of K32(F1())

y /. B is Element of bool F1()
y /. x is Element of bool F1()
B - 1 is V30() V31() V32() ext-real set
y . B is set

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

FT . x is Element of bool F1()

y /. y is Element of bool F1()

y /. (y + 1) is Element of bool F1()
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 F1()
(y - 1) + 1 is V30() V31() V32() ext-real set
FT . ((y - 1) + 1) is set
y . y is set

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

y /. (B + 1) is Element of bool F1()
F4((y /. B)) is Element of K32(F1())

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

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 F1()
(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 F1()

y /. (B + 0) is Element of bool F1()
y /. (x + 1) is Element of bool F1()
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 F1()

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
is non empty finite V50() Element of K32(NAT)
(0) is V7() V10() V11() finite Element of K32(K33(,))
is non empty finite V50() set
K33(,) is non empty finite set
K32(K33(,)) is non empty finite V50() set
[0,0] is set
{0,0} is non empty finite V50() set
is non empty finite V50() set
is non empty finite set
RelStr(# ,(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,b1) where b1 is Element of the carrier of FT : verum } is set
A is set
union { (FT,b1) where b1 is Element of the carrier of FT : verum } is 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
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
{ b1 where b1 is Element of the carrier of FT : ( not (FT,b1) misses A & not (FT,b1) misses A ` ) } is set
{ b1 where b1 is Element of the carrier of FT : S1[b1] } 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)
x ` is Element of K32( the carrier of FT)
the carrier of FT \ x is set
{ b1 where b1 is Element of the carrier of FT : ( not (FT,b1) misses x & not (FT,b1) misses x ` ) } is set
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
{ b1 where b1 is Element of the carrier of FT : ( not (FT,b1) misses A & not (FT,b1) misses A ` ) } is set
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
{ b1 where b1 is Element of the carrier of FT : ( not (FT,b1) misses A & not (FT,b1) misses A ` ) } is set
(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)
{ b1 where b1 is Element of the carrier of FT : (FT,b1) c= A } is set
{ b1 where b1 is Element of the carrier of FT : S1[b1] } is set
{ b1 where b1 is Element of the carrier of FT : not (FT,b1) misses A } is set
{ b1 where b1 is Element of the carrier of FT : S1[b1] } is set
{ b1 where b1 is Element of the carrier of FT : ( b1 in A & (FT,b1) \ {b1} misses A ) } is set
{ b1 where b1 is Element of the carrier of FT : S1[b1] } 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)
{ b1 where b1 is Element of the carrier of FT : ( b1 in A & (FT,b1) \ {b1} misses A ) } is set
A \ (FT,A) is Element of K32( the carrier of FT)
{ b1 where b1 is Element of the carrier of FT : ex b2 being Element of the carrier of FT st
( b2 in A & b1 in (FT,b2) )
}
is set

{ b1 where b1 is Element of the carrier of FT : S1[b1] } 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)
{ b1 where b1 is Element of the carrier of FT : (FT,b1) c= x } is set
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)
{ b1 where b1 is Element of the carrier of FT : not (FT,b1) misses x } is set
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)
{ b1 where b1 is Element of the carrier of FT : ( b1 in x & (FT,b1) \ {b1} misses x ) } is set
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)
{ b1 where b1 is Element of the carrier of FT : ( b1 in x & (FT,b1) \ {b1} misses x ) } is set
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)
{ b1 where b1 is Element of the carrier of FT : ex b2 being Element of the carrier of FT st
( b2 in x & b1 in (FT,b2) )
}
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
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)
{ b1 where b1 is Element of the carrier of FT : not (FT,b1) misses A } is set
(FT,A) is Element of K32( the carrier of FT)
{ b1 where b1 is Element of the carrier of FT : ex b2 being Element of the carrier of FT st
( b2 in A & b1 in (FT,b2) )
}
is set

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)
{ b1 where b1 is Element of the carrier of FT : not (FT,b1) misses {x} } is set
(FT,{x}) is Element of K32( the carrier of FT)
{ b1 where b1 is Element of the carrier of FT : ex b2 being Element of the carrier of FT st
( b2 in {x} & b1 in (FT,b2) )
}
is set

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)
{ b1 where b1 is Element of K32( the carrier of FT) : ( A c= b1 & b1 is (FT) ) } is set
meet { b1 where b1 is Element of K32( the carrier of FT) : ( A c= b1 & b1 is (FT) ) } is set
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)
{ b1 where b1 is Element of K32( the carrier of FT) : ( A c= b1 & b1 is (FT) ) } is set
union { b1 where b1 is Element of K32( the carrier of FT) : ( A c= b1 & b1 is (FT) ) } is set
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)
{ b1 where b1 is Element of the carrier of FT : not (FT,b1) misses A } is set
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)
{ b1 where b1 is Element of the carrier of FT : not (FT,b1) misses A } is set
(FT,x) is Element of K32( the carrier of FT)
{ b1 where b1 is Element of the carrier of FT : not (FT,b1) misses x } is set
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)
{ b1 where b1 is Element of the carrier of FT : not (FT,b1) misses y } is set
(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

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)
{ b1 where b1 is Element of the carrier of FT : not (FT,b1) misses y /. (len y) } is set
(FT,(y /. (len y))) /\ A is finite Element of K32( the carrier of FT)

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

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

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

y /. (c9 + 1) is finite Element of bool the carrier of FT
y /. c9 is finite Element of bool the carrier of FT
(FT,(y /. c9)) is finite Element of K32( the carrier of FT)
{ b1 where b1 is Element of the carrier of FT : not (FT,b1) misses y /. c9 } is set
(FT,(y /. c9)) /\ A is finite Element of K32( the carrier of FT)
(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)
{ b1 where b1 is Element of the carrier of FT : not (FT,b1) misses x } is set
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

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

(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

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)
{ b1 where b1 is Element of the carrier of FT : not (FT,b1) misses x /. (y + 1) } is set
(FT,(x /. (y + 1))) /\ A is finite Element of K32( the carrier of FT)

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

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)
{ b1 where b1 is Element of the carrier of FT : (FT,b1) c= A ` } is set
(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)
{ b1 where b1 is Element of the carrier of FT : not (FT,b1) misses A } is set
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)
{ b1 where b1 is Element of the carrier of FT : not (FT,b1) misses A ` } is set
(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)
{ b1 where b1 is Element of the carrier of FT : (FT,b1) c= A } is set
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
{ b1 where b1 is Element of the carrier of FT : ( not (FT,b1) misses A & not (FT,b1) misses A ` ) } is set
(FT,A) is Element of K32( the carrier of FT)
{ b1 where b1 is Element of the carrier of FT : not (FT,b1) misses A } is set
(FT,(A `)) is Element of K32( the carrier of FT)
{ b1 where b1 is Element of the carrier of FT : not (FT,b1) misses A ` } is set
(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
{ b1 where b1 is Element of the carrier of FT : ( not (FT,b1) misses A ` & not (FT,b1) misses (A `) ` ) } is set
(FT,A) is Element of K32( the carrier of FT)
{ b1 where b1 is Element of the carrier of FT : ( not (FT,b1) misses A & not (FT,b1) misses A ` ) } is set
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)
{ b1 where b1 is Element of the carrier of FT : ( b1 in x & (FT,b1) \ {b1} misses x ) } is set
x \ {A} is Element of K32( the carrier of FT)
(FT,(x \ {A})) is Element of K32( the carrier of FT)
{ b1 where b1 is Element of the carrier of FT : not (FT,b1) misses x \ {A} } is set
(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)
{ b1 where b1 is Element of the carrier of FT : ( b1 in A & (FT,b1) \ {b1} misses A ) } is 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)

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)
{ b1 where b1 is Element of the carrier of FT : not (FT,b1) misses A \ {x} } is set
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)
c9 is set
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)
{ b1 where b1 is Element of the carrier of FT : (FT,b1) c= A } is set
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)
{ b1 where b1 is Element of the carrier of FT : (FT,b1) c= A } is set
(FT,(A `)) is Element of K32( the carrier of FT)
{ b1 where b1 is Element of the carrier of FT : not (FT,b1) misses A ` } is set
(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)
{ b1 where b1 is Element of the carrier of FT : not (FT,b1) misses A } is set
(FT,(A `)) is Element of K32( the carrier of FT)
{ b1 where b1 is Element of the carrier of FT : (FT,b1) c= A ` } is set
(FT,(A `)) ` is Element of K32( the carrier of FT)
the carrier of FT \ (FT,(A `)) is set