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
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()
A is epsilon-transitive epsilon-connected ordinal natural V30() V31() V32() ext-real non negative Element of NAT
FT . A is Element of bool F1()
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 F1()
F4((FT . A)) is Element of K32(F1())
A is epsilon-transitive epsilon-connected ordinal natural V30() V31() V32() ext-real non negative Element of NAT
FT . A is Element of bool F1()
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 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
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 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()))
x is epsilon-transitive epsilon-connected ordinal natural V30() V31() V32() ext-real non negative Element of NAT
FT . x is Element of bool F1()
A is set
FT .: NAT is Element of K32((bool F1()))
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 F1()) Function-like FinSequence-like FinSequence of bool F1()
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 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
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 F1()
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 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
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 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 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 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()
B is epsilon-transitive epsilon-connected ordinal natural V30() V31() V32() ext-real non negative Element of NAT
FT . B is Element of bool F1()
F4((FT . B)) is Element of K32(F1())
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 F1()
y /. x is Element of bool F1()
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 F1()
x is epsilon-transitive epsilon-connected ordinal natural V30() V31() V32() ext-real non negative Element of NAT
FT . x is Element of bool F1()
y is epsilon-transitive epsilon-connected ordinal natural V30() V31() V32() ext-real non negative Element of NAT
y /. y is Element of bool F1()
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 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
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 F1()
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 F1()
F4((y /. B)) is Element of K32(F1())
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 F1()
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 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 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
c9 is epsilon-transitive epsilon-connected ordinal natural V30() V31() V32() ext-real non negative Element of NAT
B + c9 is epsilon-transitive epsilon-connected ordinal natural V30() V31() V32() ext-real non negative Element of NAT
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 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()
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,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
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)
{ 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)
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
c9 is epsilon-transitive epsilon-connected ordinal natural V30() V31() V32() ext-real non negative Element of NAT
c9 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V30() V31() V32() ext-real positive non negative Element of NAT
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
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)
{ 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)
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)
{ 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
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)
{ 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