:: SETLIM_2 semantic presentation

REAL is set

NAT is V1() V7() V8() V9() Element of K10(REAL)

K10(REAL) is V1() set

NAT is V1() V7() V8() V9() set

K10(NAT) is V1() set

K11(NAT,REAL) is set

K10(K11(NAT,REAL)) is V1() set

K10(K10(REAL)) is V1() set

X is V7() V8() V9() V13() V14() ext-real V58() Element of NAT

A is set

K32(A) is V1() Element of K10(K10(A))

K10(A) is V1() set

K10(K10(A)) is V1() set

K11(NAT,K32(A)) is V1() set

K10(K11(NAT,K32(A))) is V1() set

A1 is V1() V18() V21( NAT ) V22(K32(A)) Function-like V28( NAT ) V32( NAT ,K32(A)) Element of K10(K11(NAT,K32(A)))

inferior_setsequence A1 is V1() V18() V21( NAT ) V22(K32(A)) Function-like V28( NAT ) V32( NAT ,K32(A)) Element of K10(K11(NAT,K32(A)))

(inferior_setsequence A1) . X is Element of K32(A)

A1 ^\ X is V1() V18() V21( NAT ) V22(K32(A)) Function-like V28( NAT ) V32( NAT ,K32(A)) Element of K10(K11(NAT,K32(A)))

Intersection (A1 ^\ X) is Element of K10(A)

{ (A1 . b

x is Element of K10(K10(A))

meet x is Element of K10(A)

rng (A1 ^\ X) is set

meet (rng (A1 ^\ X)) is set

X is V7() V8() V9() V13() V14() ext-real V58() Element of NAT

A is set

K32(A) is V1() Element of K10(K10(A))

K10(A) is V1() set

K10(K10(A)) is V1() set

K11(NAT,K32(A)) is V1() set

K10(K11(NAT,K32(A))) is V1() set

A1 is V1() V18() V21( NAT ) V22(K32(A)) Function-like V28( NAT ) V32( NAT ,K32(A)) Element of K10(K11(NAT,K32(A)))

superior_setsequence A1 is V1() V18() V21( NAT ) V22(K32(A)) Function-like V28( NAT ) V32( NAT ,K32(A)) Element of K10(K11(NAT,K32(A)))

(superior_setsequence A1) . X is Element of K32(A)

A1 ^\ X is V1() V18() V21( NAT ) V22(K32(A)) Function-like V28( NAT ) V32( NAT ,K32(A)) Element of K10(K11(NAT,K32(A)))

Union (A1 ^\ X) is Element of K10(A)

{ (A1 . b

x is Element of K10(K10(A))

union x is Element of K10(A)

rng (A1 ^\ X) is set

union (rng (A1 ^\ X)) is set

X is set

K32(X) is V1() Element of K10(K10(X))

K10(X) is V1() set

K10(K10(X)) is V1() set

K11(NAT,K32(X)) is V1() set

K10(K11(NAT,K32(X))) is V1() set

A is V1() V18() V21( NAT ) V22(K32(X)) Function-like V28( NAT ) V32( NAT ,K32(X)) Element of K10(K11(NAT,K32(X)))

A1 is V1() V18() V21( NAT ) V22(K32(X)) Function-like V28( NAT ) V32( NAT ,K32(X)) Element of K10(K11(NAT,K32(X)))

x is V1() V18() V21( NAT ) V22(K32(X)) Function-like V28( NAT ) V32( NAT ,K32(X)) Element of K10(K11(NAT,K32(X)))

x is V1() V18() V21( NAT ) V22(K32(X)) Function-like V28( NAT ) V32( NAT ,K32(X)) Element of K10(K11(NAT,K32(X)))

n2 is V1() V18() V21( NAT ) V22(K32(X)) Function-like V28( NAT ) V32( NAT ,K32(X)) Element of K10(K11(NAT,K32(X)))

k1 is V7() V8() V9() V13() V14() ext-real V58() Element of NAT

x . k1 is set

n2 . k1 is set

x . k1 is Element of K32(X)

A . k1 is Element of K32(X)

A1 . k1 is Element of K32(X)

(A . k1) /\ (A1 . k1) is Element of K10(X)

n2 . k1 is Element of K32(X)

x is V1() V18() V21( NAT ) V22(K32(X)) Function-like V28( NAT ) V32( NAT ,K32(X)) Element of K10(K11(NAT,K32(X)))

n2 is V1() V18() V21( NAT ) V22(K32(X)) Function-like V28( NAT ) V32( NAT ,K32(X)) Element of K10(K11(NAT,K32(X)))

k1 is V1() V18() V21( NAT ) V22(K32(X)) Function-like V28( NAT ) V32( NAT ,K32(X)) Element of K10(K11(NAT,K32(X)))

k is V7() V8() V9() V13() V14() ext-real V58() Element of NAT

x . k is Element of K32(X)

k1 . k is Element of K32(X)

n2 . k is Element of K32(X)

(k1 . k) /\ (n2 . k) is Element of K10(X)

x is V1() V18() V21( NAT ) V22(K32(X)) Function-like V28( NAT ) V32( NAT ,K32(X)) Element of K10(K11(NAT,K32(X)))

x is V1() V18() V21( NAT ) V22(K32(X)) Function-like V28( NAT ) V32( NAT ,K32(X)) Element of K10(K11(NAT,K32(X)))

n2 is V1() V18() V21( NAT ) V22(K32(X)) Function-like V28( NAT ) V32( NAT ,K32(X)) Element of K10(K11(NAT,K32(X)))

k1 is V7() V8() V9() V13() V14() ext-real V58() Element of NAT

x . k1 is set

n2 . k1 is set

x . k1 is Element of K32(X)

A . k1 is Element of K32(X)

A1 . k1 is Element of K32(X)

(A . k1) \/ (A1 . k1) is Element of K10(X)

n2 . k1 is Element of K32(X)

x is V1() V18() V21( NAT ) V22(K32(X)) Function-like V28( NAT ) V32( NAT ,K32(X)) Element of K10(K11(NAT,K32(X)))

n2 is V1() V18() V21( NAT ) V22(K32(X)) Function-like V28( NAT ) V32( NAT ,K32(X)) Element of K10(K11(NAT,K32(X)))

k1 is V1() V18() V21( NAT ) V22(K32(X)) Function-like V28( NAT ) V32( NAT ,K32(X)) Element of K10(K11(NAT,K32(X)))

k is V7() V8() V9() V13() V14() ext-real V58() Element of NAT

x . k is Element of K32(X)

k1 . k is Element of K32(X)

n2 . k is Element of K32(X)

(k1 . k) \/ (n2 . k) is Element of K10(X)

x is V1() V18() V21( NAT ) V22(K32(X)) Function-like V28( NAT ) V32( NAT ,K32(X)) Element of K10(K11(NAT,K32(X)))

x is V1() V18() V21( NAT ) V22(K32(X)) Function-like V28( NAT ) V32( NAT ,K32(X)) Element of K10(K11(NAT,K32(X)))

n2 is V1() V18() V21( NAT ) V22(K32(X)) Function-like V28( NAT ) V32( NAT ,K32(X)) Element of K10(K11(NAT,K32(X)))

k1 is V7() V8() V9() V13() V14() ext-real V58() Element of NAT

x . k1 is set

n2 . k1 is set

x . k1 is Element of K32(X)

A . k1 is Element of K32(X)

A1 . k1 is Element of K32(X)

(A . k1) \ (A1 . k1) is Element of K10(X)

n2 . k1 is Element of K32(X)

x is V1() V18() V21( NAT ) V22(K32(X)) Function-like V28( NAT ) V32( NAT ,K32(X)) Element of K10(K11(NAT,K32(X)))

x is V1() V18() V21( NAT ) V22(K32(X)) Function-like V28( NAT ) V32( NAT ,K32(X)) Element of K10(K11(NAT,K32(X)))

n2 is V1() V18() V21( NAT ) V22(K32(X)) Function-like V28( NAT ) V32( NAT ,K32(X)) Element of K10(K11(NAT,K32(X)))

k1 is V7() V8() V9() V13() V14() ext-real V58() Element of NAT

x . k1 is set

n2 . k1 is set

x . k1 is Element of K32(X)

A . k1 is Element of K32(X)

A1 . k1 is Element of K32(X)

(A . k1) \+\ (A1 . k1) is Element of K10(X)

K8((A . k1),(A1 . k1)) is set

K8((A1 . k1),(A . k1)) is set

K6(K8((A . k1),(A1 . k1)),K8((A1 . k1),(A . k1))) is set

n2 . k1 is Element of K32(X)

x is V1() V18() V21( NAT ) V22(K32(X)) Function-like V28( NAT ) V32( NAT ,K32(X)) Element of K10(K11(NAT,K32(X)))

n2 is V1() V18() V21( NAT ) V22(K32(X)) Function-like V28( NAT ) V32( NAT ,K32(X)) Element of K10(K11(NAT,K32(X)))

k1 is V1() V18() V21( NAT ) V22(K32(X)) Function-like V28( NAT ) V32( NAT ,K32(X)) Element of K10(K11(NAT,K32(X)))

k is V7() V8() V9() V13() V14() ext-real V58() Element of NAT

x . k is Element of K32(X)

k1 . k is Element of K32(X)

n2 . k is Element of K32(X)

(k1 . k) \+\ (n2 . k) is Element of K10(X)

K8((k1 . k),(n2 . k)) is set

K8((n2 . k),(k1 . k)) is set

K6(K8((k1 . k),(n2 . k)),K8((n2 . k),(k1 . k))) is set

X is set

K32(X) is V1() Element of K10(K10(X))

K10(X) is V1() set

K10(K10(X)) is V1() set

K11(NAT,K32(X)) is V1() set

K10(K11(NAT,K32(X))) is V1() set

A is V1() V18() V21( NAT ) V22(K32(X)) Function-like V28( NAT ) V32( NAT ,K32(X)) Element of K10(K11(NAT,K32(X)))

A1 is V1() V18() V21( NAT ) V22(K32(X)) Function-like V28( NAT ) V32( NAT ,K32(X)) Element of K10(K11(NAT,K32(X)))

(X,A,A1) is V1() V18() V21( NAT ) V22(K32(X)) Function-like V28( NAT ) V32( NAT ,K32(X)) Element of K10(K11(NAT,K32(X)))

(X,A,A1) is V1() V18() V21( NAT ) V22(K32(X)) Function-like V28( NAT ) V32( NAT ,K32(X)) Element of K10(K11(NAT,K32(X)))

(X,A1,A) is V1() V18() V21( NAT ) V22(K32(X)) Function-like V28( NAT ) V32( NAT ,K32(X)) Element of K10(K11(NAT,K32(X)))

(X,(X,A,A1),(X,A1,A)) is V1() V18() V21( NAT ) V22(K32(X)) Function-like V28( NAT ) V32( NAT ,K32(X)) Element of K10(K11(NAT,K32(X)))

x is V7() V8() V9() V13() V14() ext-real V58() Element of NAT

(X,A,A1) . x is set

(X,(X,A,A1),(X,A1,A)) . x is set

(X,A,A1) . x is Element of K32(X)

A . x is Element of K32(X)

A1 . x is Element of K32(X)

(A . x) \+\ (A1 . x) is Element of K10(X)

K8((A . x),(A1 . x)) is set

K8((A1 . x),(A . x)) is set

K6(K8((A . x),(A1 . x)),K8((A1 . x),(A . x))) is set

(X,A,A1) . x is Element of K32(X)

(A1 . x) \ (A . x) is Element of K10(X)

((X,A,A1) . x) \/ ((A1 . x) \ (A . x)) is Element of K10(X)

(X,A1,A) . x is Element of K32(X)

((X,A,A1) . x) \/ ((X,A1,A) . x) is Element of K10(X)

(X,(X,A,A1),(X,A1,A)) . x is Element of K32(X)

X is V7() V8() V9() V13() V14() ext-real V58() Element of NAT

A is set

K32(A) is V1() Element of K10(K10(A))

K10(A) is V1() set

K10(K10(A)) is V1() set

K11(NAT,K32(A)) is V1() set

K10(K11(NAT,K32(A))) is V1() set

A1 is V1() V18() V21( NAT ) V22(K32(A)) Function-like V28( NAT ) V32( NAT ,K32(A)) Element of K10(K11(NAT,K32(A)))

A1 ^\ X is V1() V18() V21( NAT ) V22(K32(A)) Function-like V28( NAT ) V32( NAT ,K32(A)) Element of K10(K11(NAT,K32(A)))

x is V1() V18() V21( NAT ) V22(K32(A)) Function-like V28( NAT ) V32( NAT ,K32(A)) Element of K10(K11(NAT,K32(A)))

(A,A1,x) is V1() V18() V21( NAT ) V22(K32(A)) Function-like V28( NAT ) V32( NAT ,K32(A)) Element of K10(K11(NAT,K32(A)))

(A,A1,x) ^\ X is V1() V18() V21( NAT ) V22(K32(A)) Function-like V28( NAT ) V32( NAT ,K32(A)) Element of K10(K11(NAT,K32(A)))

x ^\ X is V1() V18() V21( NAT ) V22(K32(A)) Function-like V28( NAT ) V32( NAT ,K32(A)) Element of K10(K11(NAT,K32(A)))

(A,(A1 ^\ X),(x ^\ X)) is V1() V18() V21( NAT ) V22(K32(A)) Function-like V28( NAT ) V32( NAT ,K32(A)) Element of K10(K11(NAT,K32(A)))

n2 is V7() V8() V9() V13() V14() ext-real V58() Element of NAT

((A,A1,x) ^\ X) . n2 is set

(A,(A1 ^\ X),(x ^\ X)) . n2 is set

((A,A1,x) ^\ X) . n2 is Element of K32(A)

n2 + X is V7() V8() V9() V13() V14() ext-real V58() Element of NAT

(A,A1,x) . (n2 + X) is Element of K32(A)

A1 . (n2 + X) is Element of K32(A)

x . (n2 + X) is Element of K32(A)

(A1 . (n2 + X)) /\ (x . (n2 + X)) is Element of K10(A)

(A1 ^\ X) . n2 is Element of K32(A)

((A1 ^\ X) . n2) /\ (x . (n2 + X)) is Element of K10(A)

(x ^\ X) . n2 is Element of K32(A)

((A1 ^\ X) . n2) /\ ((x ^\ X) . n2) is Element of K10(A)

(A,(A1 ^\ X),(x ^\ X)) . n2 is Element of K32(A)

X is V7() V8() V9() V13() V14() ext-real V58() Element of NAT

A is set

K32(A) is V1() Element of K10(K10(A))

K10(A) is V1() set

K10(K10(A)) is V1() set

K11(NAT,K32(A)) is V1() set

K10(K11(NAT,K32(A))) is V1() set

A1 is V1() V18() V21( NAT ) V22(K32(A)) Function-like V28( NAT ) V32( NAT ,K32(A)) Element of K10(K11(NAT,K32(A)))

A1 ^\ X is V1() V18() V21( NAT ) V22(K32(A)) Function-like V28( NAT ) V32( NAT ,K32(A)) Element of K10(K11(NAT,K32(A)))

x is V1() V18() V21( NAT ) V22(K32(A)) Function-like V28( NAT ) V32( NAT ,K32(A)) Element of K10(K11(NAT,K32(A)))

(A,A1,x) is V1() V18() V21( NAT ) V22(K32(A)) Function-like V28( NAT ) V32( NAT ,K32(A)) Element of K10(K11(NAT,K32(A)))

(A,A1,x) ^\ X is V1() V18() V21( NAT ) V22(K32(A)) Function-like V28( NAT ) V32( NAT ,K32(A)) Element of K10(K11(NAT,K32(A)))

x ^\ X is V1() V18() V21( NAT ) V22(K32(A)) Function-like V28( NAT ) V32( NAT ,K32(A)) Element of K10(K11(NAT,K32(A)))

(A,(A1 ^\ X),(x ^\ X)) is V1() V18() V21( NAT ) V22(K32(A)) Function-like V28( NAT ) V32( NAT ,K32(A)) Element of K10(K11(NAT,K32(A)))

n2 is V7() V8() V9() V13() V14() ext-real V58() Element of NAT

((A,A1,x) ^\ X) . n2 is set

(A,(A1 ^\ X),(x ^\ X)) . n2 is set

((A,A1,x) ^\ X) . n2 is Element of K32(A)

n2 + X is V7() V8() V9() V13() V14() ext-real V58() Element of NAT

(A,A1,x) . (n2 + X) is Element of K32(A)

A1 . (n2 + X) is Element of K32(A)

x . (n2 + X) is Element of K32(A)

(A1 . (n2 + X)) \/ (x . (n2 + X)) is Element of K10(A)

(A1 ^\ X) . n2 is Element of K32(A)

((A1 ^\ X) . n2) \/ (x . (n2 + X)) is Element of K10(A)

(x ^\ X) . n2 is Element of K32(A)

((A1 ^\ X) . n2) \/ ((x ^\ X) . n2) is Element of K10(A)

(A,(A1 ^\ X),(x ^\ X)) . n2 is Element of K32(A)

X is V7() V8() V9() V13() V14() ext-real V58() Element of NAT

A is set

K32(A) is V1() Element of K10(K10(A))

K10(A) is V1() set

K10(K10(A)) is V1() set

K11(NAT,K32(A)) is V1() set

K10(K11(NAT,K32(A))) is V1() set

A1 is V1() V18() V21( NAT ) V22(K32(A)) Function-like V28( NAT ) V32( NAT ,K32(A)) Element of K10(K11(NAT,K32(A)))

A1 ^\ X is V1() V18() V21( NAT ) V22(K32(A)) Function-like V28( NAT ) V32( NAT ,K32(A)) Element of K10(K11(NAT,K32(A)))

x is V1() V18() V21( NAT ) V22(K32(A)) Function-like V28( NAT ) V32( NAT ,K32(A)) Element of K10(K11(NAT,K32(A)))

(A,A1,x) is V1() V18() V21( NAT ) V22(K32(A)) Function-like V28( NAT ) V32( NAT ,K32(A)) Element of K10(K11(NAT,K32(A)))

(A,A1,x) ^\ X is V1() V18() V21( NAT ) V22(K32(A)) Function-like V28( NAT ) V32( NAT ,K32(A)) Element of K10(K11(NAT,K32(A)))

x ^\ X is V1() V18() V21( NAT ) V22(K32(A)) Function-like V28( NAT ) V32( NAT ,K32(A)) Element of K10(K11(NAT,K32(A)))

(A,(A1 ^\ X),(x ^\ X)) is V1() V18() V21( NAT ) V22(K32(A)) Function-like V28( NAT ) V32( NAT ,K32(A)) Element of K10(K11(NAT,K32(A)))

n2 is V7() V8() V9() V13() V14() ext-real V58() Element of NAT

((A,A1,x) ^\ X) . n2 is set

(A,(A1 ^\ X),(x ^\ X)) . n2 is set

((A,A1,x) ^\ X) . n2 is Element of K32(A)

n2 + X is V7() V8() V9() V13() V14() ext-real V58() Element of NAT

(A,A1,x) . (n2 + X) is Element of K32(A)

A1 . (n2 + X) is Element of K32(A)

x . (n2 + X) is Element of K32(A)

(A1 . (n2 + X)) \ (x . (n2 + X)) is Element of K10(A)

(A1 ^\ X) . n2 is Element of K32(A)

((A1 ^\ X) . n2) \ (x . (n2 + X)) is Element of K10(A)

(x ^\ X) . n2 is Element of K32(A)

((A1 ^\ X) . n2) \ ((x ^\ X) . n2) is Element of K10(A)

(A,(A1 ^\ X),(x ^\ X)) . n2 is Element of K32(A)

X is V7() V8() V9() V13() V14() ext-real V58() Element of NAT

A is set

K32(A) is V1() Element of K10(K10(A))

K10(A) is V1() set

K10(K10(A)) is V1() set

K11(NAT,K32(A)) is V1() set

K10(K11(NAT,K32(A))) is V1() set

A1 is V1() V18() V21( NAT ) V22(K32(A)) Function-like V28( NAT ) V32( NAT ,K32(A)) Element of K10(K11(NAT,K32(A)))

A1 ^\ X is V1() V18() V21( NAT ) V22(K32(A)) Function-like V28( NAT ) V32( NAT ,K32(A)) Element of K10(K11(NAT,K32(A)))

x is V1() V18() V21( NAT ) V22(K32(A)) Function-like V28( NAT ) V32( NAT ,K32(A)) Element of K10(K11(NAT,K32(A)))

(A,A1,x) is V1() V18() V21( NAT ) V22(K32(A)) Function-like V28( NAT ) V32( NAT ,K32(A)) Element of K10(K11(NAT,K32(A)))

(A,A1,x) ^\ X is V1() V18() V21( NAT ) V22(K32(A)) Function-like V28( NAT ) V32( NAT ,K32(A)) Element of K10(K11(NAT,K32(A)))

x ^\ X is V1() V18() V21( NAT ) V22(K32(A)) Function-like V28( NAT ) V32( NAT ,K32(A)) Element of K10(K11(NAT,K32(A)))

(A,(A1 ^\ X),(x ^\ X)) is V1() V18() V21( NAT ) V22(K32(A)) Function-like V28( NAT ) V32( NAT ,K32(A)) Element of K10(K11(NAT,K32(A)))

n2 is V7() V8() V9() V13() V14() ext-real V58() Element of NAT

((A,A1,x) ^\ X) . n2 is set

(A,(A1 ^\ X),(x ^\ X)) . n2 is set

((A,A1,x) ^\ X) . n2 is Element of K32(A)

n2 + X is V7() V8() V9() V13() V14() ext-real V58() Element of NAT

(A,A1,x) . (n2 + X) is Element of K32(A)

A1 . (n2 + X) is Element of K32(A)

x . (n2 + X) is Element of K32(A)

(A1 . (n2 + X)) \+\ (x . (n2 + X)) is Element of K10(A)

K8((A1 . (n2 + X)),(x . (n2 + X))) is set

K8((x . (n2 + X)),(A1 . (n2 + X))) is set

K6(K8((A1 . (n2 + X)),(x . (n2 + X))),K8((x . (n2 + X)),(A1 . (n2 + X)))) is set

(A1 ^\ X) . n2 is Element of K32(A)

((A1 ^\ X) . n2) \+\ (x . (n2 + X)) is Element of K10(A)

K8(((A1 ^\ X) . n2),(x . (n2 + X))) is set

K8((x . (n2 + X)),((A1 ^\ X) . n2)) is set

K6(K8(((A1 ^\ X) . n2),(x . (n2 + X))),K8((x . (n2 + X)),((A1 ^\ X) . n2))) is set

(x ^\ X) . n2 is Element of K32(A)

((A1 ^\ X) . n2) \+\ ((x ^\ X) . n2) is Element of K10(A)

K8(((A1 ^\ X) . n2),((x ^\ X) . n2)) is set

K8(((x ^\ X) . n2),((A1 ^\ X) . n2)) is set

K6(K8(((A1 ^\ X) . n2),((x ^\ X) . n2)),K8(((x ^\ X) . n2),((A1 ^\ X) . n2))) is set

(A,(A1 ^\ X),(x ^\ X)) . n2 is Element of K32(A)

X is set

K32(X) is V1() Element of K10(K10(X))

K10(X) is V1() set

K10(K10(X)) is V1() set

K11(NAT,K32(X)) is V1() set

K10(K11(NAT,K32(X))) is V1() set

A is V1() V18() V21( NAT ) V22(K32(X)) Function-like V28( NAT ) V32( NAT ,K32(X)) Element of K10(K11(NAT,K32(X)))

Union A is Element of K10(X)

A1 is V1() V18() V21( NAT ) V22(K32(X)) Function-like V28( NAT ) V32( NAT ,K32(X)) Element of K10(K11(NAT,K32(X)))

(X,A,A1) is V1() V18() V21( NAT ) V22(K32(X)) Function-like V28( NAT ) V32( NAT ,K32(X)) Element of K10(K11(NAT,K32(X)))

Union (X,A,A1) is Element of K10(X)

Union A1 is Element of K10(X)

(Union A) /\ (Union A1) is Element of K10(X)

x is set

n2 is V7() V8() V9() V13() V14() ext-real V58() Element of NAT

(X,A,A1) . n2 is Element of K32(X)

A . n2 is Element of K32(X)

A1 . n2 is Element of K32(X)

(A . n2) /\ (A1 . n2) is Element of K10(X)

X is set

K32(X) is V1() Element of K10(K10(X))

K10(X) is V1() set

K10(K10(X)) is V1() set

K11(NAT,K32(X)) is V1() set

K10(K11(NAT,K32(X))) is V1() set

A is V1() V18() V21( NAT ) V22(K32(X)) Function-like V28( NAT ) V32( NAT ,K32(X)) Element of K10(K11(NAT,K32(X)))

Union A is Element of K10(X)

A1 is V1() V18() V21( NAT ) V22(K32(X)) Function-like V28( NAT ) V32( NAT ,K32(X)) Element of K10(K11(NAT,K32(X)))

(X,A,A1) is V1() V18() V21( NAT ) V22(K32(X)) Function-like V28( NAT ) V32( NAT ,K32(X)) Element of K10(K11(NAT,K32(X)))

Union (X,A,A1) is Element of K10(X)

Union A1 is Element of K10(X)

(Union A) \/ (Union A1) is Element of K10(X)

x is set

n2 is V7() V8() V9() V13() V14() ext-real V58() Element of NAT

(X,A,A1) . n2 is Element of K32(X)

A . n2 is Element of K32(X)

A1 . n2 is Element of K32(X)

(A . n2) \/ (A1 . n2) is Element of K10(X)

x is set

n2 is V7() V8() V9() V13() V14() ext-real V58() Element of NAT

A . n2 is Element of K32(X)

A1 . n2 is Element of K32(X)

(A . n2) \/ (A1 . n2) is Element of K10(X)

(X,A,A1) . n2 is Element of K32(X)

n2 is V7() V8() V9() V13() V14() ext-real V58() Element of NAT

A1 . n2 is Element of K32(X)

A . n2 is Element of K32(X)

(A . n2) \/ (A1 . n2) is Element of K10(X)

(X,A,A1) . n2 is Element of K32(X)

X is set

K32(X) is V1() Element of K10(K10(X))

K10(X) is V1() set

K10(K10(X)) is V1() set

K11(NAT,K32(X)) is V1() set

K10(K11(NAT,K32(X))) is V1() set

A is V1() V18() V21( NAT ) V22(K32(X)) Function-like V28( NAT ) V32( NAT ,K32(X)) Element of K10(K11(NAT,K32(X)))

Union A is Element of K10(X)

A1 is V1() V18() V21( NAT ) V22(K32(X)) Function-like V28( NAT ) V32( NAT ,K32(X)) Element of K10(K11(NAT,K32(X)))

Union A1 is Element of K10(X)

(Union A) \ (Union A1) is Element of K10(X)

(X,A,A1) is V1() V18() V21( NAT ) V22(K32(X)) Function-like V28( NAT ) V32( NAT ,K32(X)) Element of K10(K11(NAT,K32(X)))

Union (X,A,A1) is Element of K10(X)

x is set

n2 is V7() V8() V9() V13() V14() ext-real V58() Element of NAT

A . n2 is Element of K32(X)

A1 . n2 is Element of K32(X)

(A . n2) \ (A1 . n2) is Element of K10(X)

(X,A,A1) . n2 is Element of K32(X)

X is set

K32(X) is V1() Element of K10(K10(X))

K10(X) is V1() set

K10(K10(X)) is V1() set

K11(NAT,K32(X)) is V1() set

K10(K11(NAT,K32(X))) is V1() set

A is V1() V18() V21( NAT ) V22(K32(X)) Function-like V28( NAT ) V32( NAT ,K32(X)) Element of K10(K11(NAT,K32(X)))

Union A is Element of K10(X)

A1 is V1() V18() V21( NAT ) V22(K32(X)) Function-like V28( NAT ) V32( NAT ,K32(X)) Element of K10(K11(NAT,K32(X)))

Union A1 is Element of K10(X)

(Union A) \+\ (Union A1) is Element of K10(X)

K8((Union A),(Union A1)) is set

K8((Union A1),(Union A)) is set

K6(K8((Union A),(Union A1)),K8((Union A1),(Union A))) is set

(X,A,A1) is V1() V18() V21( NAT ) V22(K32(X)) Function-like V28( NAT ) V32( NAT ,K32(X)) Element of K10(K11(NAT,K32(X)))

Union (X,A,A1) is Element of K10(X)

(Union A) \ (Union A1) is Element of K10(X)

(X,A,A1) is V1() V18() V21( NAT ) V22(K32(X)) Function-like V28( NAT ) V32( NAT ,K32(X)) Element of K10(K11(NAT,K32(X)))

Union (X,A,A1) is Element of K10(X)

(Union A1) \ (Union A) is Element of K10(X)

(X,A1,A) is V1() V18() V21( NAT ) V22(K32(X)) Function-like V28( NAT ) V32( NAT ,K32(X)) Element of K10(K11(NAT,K32(X)))

Union (X,A1,A) is Element of K10(X)

(Union (X,A,A1)) \/ (Union (X,A1,A)) is Element of K10(X)

(X,(X,A,A1),(X,A1,A)) is V1() V18() V21( NAT ) V22(K32(X)) Function-like V28( NAT ) V32( NAT ,K32(X)) Element of K10(K11(NAT,K32(X)))

Union (X,(X,A,A1),(X,A1,A)) is Element of K10(X)

X is set

K32(X) is V1() Element of K10(K10(X))

K10(X) is V1() set

K10(K10(X)) is V1() set

K11(NAT,K32(X)) is V1() set

K10(K11(NAT,K32(X))) is V1() set

A is V1() V18() V21( NAT ) V22(K32(X)) Function-like V28( NAT ) V32( NAT ,K32(X)) Element of K10(K11(NAT,K32(X)))

Intersection A is Element of K10(X)

A1 is V1() V18() V21( NAT ) V22(K32(X)) Function-like V28( NAT ) V32( NAT ,K32(X)) Element of K10(K11(NAT,K32(X)))

(X,A,A1) is V1() V18() V21( NAT ) V22(K32(X)) Function-like V28( NAT ) V32( NAT ,K32(X)) Element of K10(K11(NAT,K32(X)))

Intersection (X,A,A1) is Element of K10(X)

Intersection A1 is Element of K10(X)

(Intersection A) /\ (Intersection A1) is Element of K10(X)

x is set

n2 is V7() V8() V9() V13() V14() ext-real V58() Element of NAT

(X,A,A1) . n2 is Element of K32(X)

A . n2 is Element of K32(X)

A1 . n2 is Element of K32(X)

(A . n2) /\ (A1 . n2) is Element of K10(X)

x is set

n2 is V7() V8() V9() V13() V14() ext-real V58() Element of NAT

A . n2 is Element of K32(X)

A1 . n2 is Element of K32(X)

(A . n2) /\ (A1 . n2) is Element of K10(X)

(X,A,A1) . n2 is Element of K32(X)

X is set

K32(X) is V1() Element of K10(K10(X))

K10(X) is V1() set

K10(K10(X)) is V1() set

K11(NAT,K32(X)) is V1() set

K10(K11(NAT,K32(X))) is V1() set

A is V1() V18() V21( NAT ) V22(K32(X)) Function-like V28( NAT ) V32( NAT ,K32(X)) Element of K10(K11(NAT,K32(X)))

Intersection A is Element of K10(X)

A1 is V1() V18() V21( NAT ) V22(K32(X)) Function-like V28( NAT ) V32( NAT ,K32(X)) Element of K10(K11(NAT,K32(X)))

Intersection A1 is Element of K10(X)

(Intersection A) \/ (Intersection A1) is Element of K10(X)

(X,A,A1) is V1() V18() V21( NAT ) V22(K32(X)) Function-like V28( NAT ) V32( NAT ,K32(X)) Element of K10(K11(NAT,K32(X)))

Intersection (X,A,A1) is Element of K10(X)

x is set

n2 is V7() V8() V9() V13() V14() ext-real V58() Element of NAT

A . n2 is Element of K32(X)

A1 . n2 is Element of K32(X)

(A . n2) \/ (A1 . n2) is Element of K10(X)

(X,A,A1) . n2 is Element of K32(X)

n2 is V7() V8() V9() V13() V14() ext-real V58() Element of NAT

A1 . n2 is Element of K32(X)

A . n2 is Element of K32(X)

(A . n2) \/ (A1 . n2) is Element of K10(X)

(X,A,A1) . n2 is Element of K32(X)

X is set

K32(X) is V1() Element of K10(K10(X))

K10(X) is V1() set

K10(K10(X)) is V1() set

K11(NAT,K32(X)) is V1() set

K10(K11(NAT,K32(X))) is V1() set

A is V1() V18() V21( NAT ) V22(K32(X)) Function-like V28( NAT ) V32( NAT ,K32(X)) Element of K10(K11(NAT,K32(X)))

Intersection A is Element of K10(X)

A1 is V1() V18() V21( NAT ) V22(K32(X)) Function-like V28( NAT ) V32( NAT ,K32(X)) Element of K10(K11(NAT,K32(X)))

(X,A,A1) is V1() V18() V21( NAT ) V22(K32(X)) Function-like V28( NAT ) V32( NAT ,K32(X)) Element of K10(K11(NAT,K32(X)))

Intersection (X,A,A1) is Element of K10(X)

Intersection A1 is Element of K10(X)

(Intersection A) \ (Intersection A1) is Element of K10(X)

x is set

n2 is V7() V8() V9() V13() V14() ext-real V58() Element of NAT

(X,A,A1) . n2 is Element of K32(X)

A . n2 is Element of K32(X)

A1 . n2 is Element of K32(X)

(A . n2) \ (A1 . n2) is Element of K10(X)

0 is V7() V8() V9() V13() V14() ext-real V58() Element of NAT

the V1() V7() V8() V9() V11() V12() V13() V14() ext-real V58() set is V1() V7() V8() V9() V11() V12() V13() V14() ext-real V58() set

A1 . 0 is Element of K32(X)

X is set

K32(X) is V1() Element of K10(K10(X))

K10(X) is V1() set

K10(K10(X)) is V1() set

K11(NAT,K32(X)) is V1() set

K10(K11(NAT,K32(X))) is V1() set

A1 is Element of K10(X)

A is V1() V18() V21( NAT ) V22(K32(X)) Function-like V28( NAT ) V32( NAT ,K32(X)) Element of K10(K11(NAT,K32(X)))

x is V1() V18() V21( NAT ) V22(K32(X)) Function-like V28( NAT ) V32( NAT ,K32(X)) Element of K10(K11(NAT,K32(X)))

x is V1() V18() V21( NAT ) V22(K32(X)) Function-like V28( NAT ) V32( NAT ,K32(X)) Element of K10(K11(NAT,K32(X)))

n2 is V1() V18() V21( NAT ) V22(K32(X)) Function-like V28( NAT ) V32( NAT ,K32(X)) Element of K10(K11(NAT,K32(X)))

k1 is V7() V8() V9() V13() V14() ext-real V58() Element of NAT

x . k1 is set

n2 . k1 is set

x . k1 is Element of K32(X)

A . k1 is Element of K32(X)

A1 /\ (A . k1) is Element of K10(X)

n2 . k1 is Element of K32(X)

x is V1() V18() V21( NAT ) V22(K32(X)) Function-like V28( NAT ) V32( NAT ,K32(X)) Element of K10(K11(NAT,K32(X)))

x is V1() V18() V21( NAT ) V22(K32(X)) Function-like V28( NAT ) V32( NAT ,K32(X)) Element of K10(K11(NAT,K32(X)))

n2 is V1() V18() V21( NAT ) V22(K32(X)) Function-like V28( NAT ) V32( NAT ,K32(X)) Element of K10(K11(NAT,K32(X)))

k1 is V7() V8() V9() V13() V14() ext-real V58() Element of NAT

x . k1 is set

n2 . k1 is set

x . k1 is Element of K32(X)

A . k1 is Element of K32(X)

A1 \/ (A . k1) is Element of K10(X)

n2 . k1 is Element of K32(X)

x is V1() V18() V21( NAT ) V22(K32(X)) Function-like V28( NAT ) V32( NAT ,K32(X)) Element of K10(K11(NAT,K32(X)))

x is V1() V18() V21( NAT ) V22(K32(X)) Function-like V28( NAT ) V32( NAT ,K32(X)) Element of K10(K11(NAT,K32(X)))

n2 is V1() V18() V21( NAT ) V22(K32(X)) Function-like V28( NAT ) V32( NAT ,K32(X)) Element of K10(K11(NAT,K32(X)))

k1 is V7() V8() V9() V13() V14() ext-real V58() Element of NAT

x . k1 is set

n2 . k1 is set

x . k1 is Element of K32(X)

A . k1 is Element of K32(X)

A1 \ (A . k1) is Element of K10(X)

n2 . k1 is Element of K32(X)

x is V1() V18() V21( NAT ) V22(K32(X)) Function-like V28( NAT ) V32( NAT ,K32(X)) Element of K10(K11(NAT,K32(X)))

x is V1() V18() V21( NAT ) V22(K32(X)) Function-like V28( NAT ) V32( NAT ,K32(X)) Element of K10(K11(NAT,K32(X)))

n2 is V1() V18() V21( NAT ) V22(K32(X)) Function-like V28( NAT ) V32( NAT ,K32(X)) Element of K10(K11(NAT,K32(X)))

k1 is V7() V8() V9() V13() V14() ext-real V58() Element of NAT

x . k1 is set

n2 . k1 is set

x . k1 is Element of K32(X)

A . k1 is Element of K32(X)

(A . k1) \ A1 is Element of K10(X)

n2 . k1 is Element of K32(X)

x is V1() V18() V21( NAT ) V22(K32(X)) Function-like V28( NAT ) V32( NAT ,K32(X)) Element of K10(K11(NAT,K32(X)))

x is V1() V18() V21( NAT ) V22(K32(X)) Function-like V28( NAT ) V32( NAT ,K32(X)) Element of K10(K11(NAT,K32(X)))

n2 is V1() V18() V21( NAT ) V22(K32(X)) Function-like V28( NAT ) V32( NAT ,K32(X)) Element of K10(K11(NAT,K32(X)))

k1 is V7() V8() V9() V13() V14() ext-real V58() Element of NAT

x . k1 is set

n2 . k1 is set

x . k1 is Element of K32(X)

A . k1 is Element of K32(X)

A1 \+\ (A . k1) is Element of K10(X)

K8(A1,(A . k1)) is set

K8((A . k1),A1) is set

K6(K8(A1,(A . k1)),K8((A . k1),A1)) is set

n2 . k1 is Element of K32(X)

X is set

K10(X) is V1() set

K32(X) is V1() Element of K10(K10(X))

K10(K10(X)) is V1() set

K11(NAT,K32(X)) is V1() set

K10(K11(NAT,K32(X))) is V1() set

A is Element of K10(X)

A1 is V1() V18() V21( NAT ) V22(K32(X)) Function-like V28( NAT ) V32( NAT ,K32(X)) Element of K10(K11(NAT,K32(X)))

(X,A1,A) is V1() V18() V21( NAT ) V22(K32(X)) Function-like V28( NAT ) V32( NAT ,K32(X)) Element of K10(K11(NAT,K32(X)))

(X,A1,A) is V1() V18() V21( NAT ) V22(K32(X)) Function-like V28( NAT ) V32( NAT ,K32(X)) Element of K10(K11(NAT,K32(X)))

(X,A1,A) is V1() V18() V21( NAT ) V22(K32(X)) Function-like V28( NAT ) V32( NAT ,K32(X)) Element of K10(K11(NAT,K32(X)))

(X,(X,A1,A),(X,A1,A)) is V1() V18() V21( NAT ) V22(K32(X)) Function-like V28( NAT ) V32( NAT ,K32(X)) Element of K10(K11(NAT,K32(X)))

x is V7() V8() V9() V13() V14() ext-real V58() Element of NAT

(X,A1,A) . x is set

(X,(X,A1,A),(X,A1,A)) . x is set

(X,A1,A) . x is Element of K32(X)

A1 . x is Element of K32(X)

A \+\ (A1 . x) is Element of K10(X)

K8(A,(A1 . x)) is set

K8((A1 . x),A) is set

K6(K8(A,(A1 . x)),K8((A1 . x),A)) is set

(X,A1,A) . x is Element of K32(X)

(A1 . x) \ A is Element of K10(X)

((X,A1,A) . x) \/ ((A1 . x) \ A) is Element of K10(X)

(X,A1,A) . x is Element of K32(X)

((X,A1,A) . x) \/ ((X,A1,A) . x) is Element of K10(X)

(X,(X,A1,A),(X,A1,A)) . x is Element of K32(X)

X is V7() V8() V9() V13() V14() ext-real V58() Element of NAT

A is set

K10(A) is V1() set

K32(A) is V1() Element of K10(K10(A))

K10(K10(A)) is V1() set

K11(NAT,K32(A)) is V1() set

K10(K11(NAT,K32(A))) is V1() set

A1 is Element of K10(A)

x is V1() V18() V21( NAT ) V22(K32(A)) Function-like V28( NAT ) V32( NAT ,K32(A)) Element of K10(K11(NAT,K32(A)))

(A,x,A1) is V1() V18() V21( NAT ) V22(K32(A)) Function-like V28( NAT ) V32( NAT ,K32(A)) Element of K10(K11(NAT,K32(A)))

(A,x,A1) ^\ X is V1() V18() V21( NAT ) V22(K32(A)) Function-like V28( NAT ) V32( NAT ,K32(A)) Element of K10(K11(NAT,K32(A)))

x ^\ X is V1() V18() V21( NAT ) V22(K32(A)) Function-like V28( NAT ) V32( NAT ,K32(A)) Element of K10(K11(NAT,K32(A)))

(A,(x ^\ X),A1) is V1() V18() V21( NAT ) V22(K32(A)) Function-like V28( NAT ) V32( NAT ,K32(A)) Element of K10(K11(NAT,K32(A)))

n2 is V7() V8() V9() V13() V14() ext-real V58() Element of NAT

((A,x,A1) ^\ X) . n2 is set

(A,(x ^\ X),A1) . n2 is set

((A,x,A1) ^\ X) . n2 is Element of K32(A)

n2 + X is V7() V8() V9() V13() V14() ext-real V58() Element of NAT

(A,x,A1) . (n2 + X) is Element of K32(A)

x . (n2 + X) is Element of K32(A)

A1 /\ (x . (n2 + X)) is Element of K10(A)

(x ^\ X) . n2 is Element of K32(A)

A1 /\ ((x ^\ X) . n2) is Element of K10(A)

(A,(x ^\ X),A1) . n2 is Element of K32(A)

X is V7() V8() V9() V13() V14() ext-real V58() Element of NAT

A is set

K10(A) is V1() set

K32(A) is V1() Element of K10(K10(A))

K10(K10(A)) is V1() set

K11(NAT,K32(A)) is V1() set

K10(K11(NAT,K32(A))) is V1() set

A1 is Element of K10(A)

x is V1() V18() V21( NAT ) V22(K32(A)) Function-like V28( NAT ) V32( NAT ,K32(A)) Element of K10(K11(NAT,K32(A)))

(A,x,A1) is V1() V18() V21( NAT ) V22(K32(A)) Function-like V28( NAT ) V32( NAT ,K32(A)) Element of K10(K11(NAT,K32(A)))

(A,x,A1) ^\ X is V1() V18() V21( NAT ) V22(K32(A)) Function-like V28( NAT ) V32( NAT ,K32(A)) Element of K10(K11(NAT,K32(A)))

x ^\ X is V1() V18() V21( NAT ) V22(K32(A)) Function-like V28( NAT ) V32( NAT ,K32(A)) Element of K10(K11(NAT,K32(A)))

(A,(x ^\ X),A1) is V1() V18() V21( NAT ) V22(K32(A)) Function-like V28( NAT ) V32( NAT ,K32(A)) Element of K10(K11(NAT,K32(A)))

n2 is V7() V8() V9() V13() V14() ext-real V58() Element of NAT

((A,x,A1) ^\ X) . n2 is set

(A,(x ^\ X),A1) . n2 is set

((A,x,A1) ^\ X) . n2 is Element of K32(A)

n2 + X is V7() V8() V9() V13() V14() ext-real V58() Element of NAT

(A,x,A1) . (n2 + X) is Element of K32(A)

x . (n2 + X) is Element of K32(A)

A1 \/ (x . (n2 + X)) is Element of K10(A)

(x ^\ X) . n2 is Element of K32(A)

A1 \/ ((x ^\ X) . n2) is Element of K10(A)

(A,(x ^\ X),A1) . n2 is Element of K32(A)

X is V7() V8() V9() V13() V14() ext-real V58() Element of NAT

A is set

K10(A) is V1() set

K32(A) is V1() Element of K10(K10(A))

K10(K10(A)) is V1() set

K11(NAT,K32(A)) is V1() set

K10(K11(NAT,K32(A))) is V1() set

A1 is Element of K10(A)

x is V1() V18() V21( NAT ) V22(K32(A)) Function-like V28( NAT ) V32( NAT ,K32(A)) Element of K10(K11(NAT,K32(A)))

(A,x,A1) is V1() V18() V21( NAT ) V22(K32(A)) Function-like V28( NAT ) V32( NAT ,K32(A)) Element of K10(K11(NAT,K32(A)))

(A,x,A1) ^\ X is V1() V18() V21( NAT ) V22(K32(A)) Function-like V28( NAT ) V32( NAT ,K32(A)) Element of K10(K11(NAT,K32(A)))

x ^\ X is V1() V18() V21( NAT ) V22(K32(A)) Function-like V28( NAT ) V32( NAT ,K32(A)) Element of K10(K11(NAT,K32(A)))

(A,(x ^\ X),A1) is V1() V18() V21( NAT ) V22(K32(A)) Function-like V28( NAT ) V32( NAT ,K32(A)) Element of K10(K11(NAT,K32(A)))

n2 is V7() V8() V9() V13() V14() ext-real V58() Element of NAT

((A,x,A1) ^\ X) . n2 is set

(A,(x ^\ X),A1) . n2 is set

((A,x,A1) ^\ X) . n2 is Element of K32(A)

n2 + X is V7() V8() V9() V13() V14() ext-real V58() Element of NAT

(A,x,A1) . (n2 + X) is Element of K32(A)

x . (n2 + X) is Element of K32(A)

A1 \ (x . (n2 + X)) is Element of K10(A)

(x ^\ X) . n2 is Element of K32(A)

A1 \ ((x ^\ X) . n2) is Element of K10(A)

(A,(x ^\ X),A1) . n2 is Element of K32(A)

X is V7() V8() V9() V13() V14() ext-real V58() Element of NAT

A is set

K10(A) is V1() set

K32(A) is V1() Element of K10(K10(A))

K10(K10(A)) is V1() set

K11(NAT,K32(A)) is V1() set

K10(K11(NAT,K32(A))) is V1() set

A1 is Element of K10(A)

x is V1() V18() V21( NAT ) V22(K32(A)) Function-like V28( NAT ) V32( NAT ,K32(A)) Element of K10(K11(NAT,K32(A)))

(A,x,A1) is V1() V18() V21( NAT ) V22(K32(A)) Function-like V28( NAT ) V32( NAT ,K32(A)) Element of K10(K11(NAT,K32(A)))

(A,x,A1) ^\ X is V1() V18() V21( NAT ) V22(K32(A)) Function-like V28( NAT ) V32( NAT ,K32(A)) Element of K10(K11(NAT,K32(A)))

x ^\ X is V1() V18() V21( NAT ) V22(K32(A)) Function-like V28( NAT ) V32( NAT ,K32(A)) Element of K10(K11(NAT,K32(A)))

(A,(x ^\ X),A1) is V1() V18() V21( NAT ) V22(K32(A)) Function-like V28( NAT ) V32( NAT ,K32(A)) Element of K10(K11(NAT,K32(A)))

n2 is V7() V8() V9() V13() V14() ext-real V58() Element of NAT

((A,x,A1) ^\ X) . n2 is set

(A,(x ^\ X),A1) . n2 is set

((A,x,A1) ^\ X) . n2 is Element of K32(A)

n2 + X is V7() V8() V9() V13() V14() ext-real V58() Element of NAT

(A,x,A1) . (n2 + X) is Element of K32(A)

x . (n2 + X) is Element of K32(A)

(x . (n2 + X)) \ A1 is Element of K10(A)

(x ^\ X) . n2 is Element of K32(A)

((x ^\ X) . n2) \ A1 is Element of K10(A)

(A,(x ^\ X),A1) . n2 is Element of K32(A)

X is V7() V8() V9() V13() V14() ext-real V58() Element of NAT

A is set

K10(A) is V1() set

K32(A) is V1() Element of K10(K10(A))

K10(K10(A)) is V1() set

K11(NAT,K32(A)) is V1() set

K10(K11(NAT,K32(A))) is V1() set

A1 is Element of K10(A)

x is V1() V18() V21( NAT ) V22(K32(A)) Function-like V28( NAT ) V32( NAT ,K32(A)) Element of K10(K11(NAT,K32(A)))

(A,x,A1) is V1() V18() V21( NAT ) V22(K32(A)) Function-like V28( NAT ) V32( NAT ,K32(A)) Element of K10(K11(NAT,K32(A)))

(A,x,A1) ^\ X is V1() V18() V21( NAT ) V22(K32(A)) Function-like V28( NAT ) V32( NAT ,K32(A)) Element of K10(K11(NAT,K32(A)))

x ^\ X is V1() V18() V21( NAT ) V22(K32(A)) Function-like V28( NAT ) V32( NAT ,K32(A)) Element of K10(K11(NAT,K32(A)))

(A,(x ^\ X),A1) is V1() V18() V21( NAT ) V22(K32(A)) Function-like V28( NAT ) V32( NAT ,K32(A)) Element of K10(K11(NAT,K32(A)))

n2 is V7() V8() V9() V13() V14() ext-real V58() Element of NAT

((A,x,A1) ^\ X) . n2 is set

(A,(x ^\ X),A1) . n2 is set

((A,x,A1) ^\ X) . n2 is Element of K32(A)

n2 + X is V7() V8() V9() V13() V14() ext-real V58() Element of NAT

(A,x,A1) . (n2 + X) is Element of K32(A)

x . (n2 + X) is Element of K32(A)

A1 \+\ (x . (n2 + X)) is Element of K10(A)

K8(A1,(x . (n2 + X))) is set

K8((x . (n2 + X)),A1) is set

K6(K8(A1,(x . (n2 + X))),K8((x . (n2 + X)),A1)) is set

(x ^\ X) . n2 is Element of K32(A)

A1 \+\ ((x ^\ X) . n2) is Element of K10(A)

K8(A1,((x ^\ X) . n2)) is set

K8(((x ^\ X) . n2),A1) is set

K6(K8(A1,((x ^\ X) . n2)),K8(((x ^\ X) . n2),A1)) is set

(A,(x ^\ X),A1) . n2 is Element of K32(A)

X is set

K10(X) is V1() set

K32(X) is V1() Element of K10(K10(X))

K10(K10(X)) is V1() set

K11(NAT,K32(X)) is V1() set

K10(K11(NAT,K32(X))) is V1() set

A is Element of K10(X)

A1 is V1() V18() V21( NAT ) V22(K32(X)) Function-like V28( NAT ) V32( NAT ,K32(X)) Element of K10(K11(NAT,K32(X)))

(X,A1,A) is V1() V18() V21( NAT ) V22(K32(X)) Function-like V28( NAT ) V32( NAT ,K32(X)) Element of K10(K11(NAT,K32(X)))

x is V7() V8() V9() V13() V14() ext-real V58() Element of NAT

(X,A1,A) . x is Element of K32(X)

n2 is V7() V8() V9() V13() V14() ext-real V58() Element of NAT

(X,A1,A) . n2 is Element of K32(X)

A1 . n2 is Element of K32(X)

A1 . x is Element of K32(X)

A /\ (A1 . n2) is Element of K10(X)

A /\ (A1 . x) is Element of K10(X)

X is set

K10(X) is V1() set

K32(X) is V1() Element of K10(K10(X))

K10(K10(X)) is V1() set

K11(NAT,K32(X)) is V1() set

K10(K11(NAT,K32(X))) is V1() set

A is Element of K10(X)

A1 is V1() V18() V21( NAT ) V22(K32(X)) Function-like V28( NAT ) V32( NAT ,K32(X)) Element of K10(K11(NAT,K32(X)))

(X,A1,A) is V1() V18() V21( NAT ) V22(K32(X)) Function-like V28( NAT ) V32( NAT ,K32(X)) Element of K10(K11(NAT,K32(X)))

x is V7() V8() V9() V13() V14() ext-real V58() Element of NAT

(X,A1,A) . x is Element of K32(X)

n2 is V7() V8() V9() V13() V14() ext-real V58() Element of NAT

(X,A1,A) . n2 is Element of K32(X)

A1 . x is Element of K32(X)

A1 . n2 is Element of K32(X)

A /\ (A1 . x) is Element of K10(X)

A /\ (A1 . n2) is Element of K10(X)

X is set

K10(X) is V1() set

K32(X) is V1() Element of K10(K10(X))

K10(K10(X)) is V1() set

K11(NAT,K32(X)) is V1() set

K10(K11(NAT,K32(X))) is V1() set

A is Element of K10(X)

A1 is V1() V18() V21( NAT ) V22(K32(X)) Function-like V28( NAT ) V32( NAT ,K32(X)) Element of K10(K11(NAT,K32(X)))

(X,A1,A) is V1() V18() V21( NAT ) V22(K32(X)) Function-like V28( NAT ) V32( NAT ,K32(X)) Element of K10(K11(NAT,K32(X)))

X is set

K10(X) is V1() set

K32(X) is V1() Element of K10(K10(X))

K10(K10(X)) is V1() set

K11(NAT,K32(X)) is V1() set

K10(K11(NAT,K32(X))) is V1() set

A is Element of K10(X)

A1 is V1() V18() V21( NAT ) V22(K32(X)) Function-like V28( NAT ) V32( NAT ,K32(X)) Element of K10(K11(NAT,K32(X)))

(X,A1,A) is V1() V18() V21( NAT ) V22(K32(X)) Function-like V28( NAT ) V32( NAT ,K32(X)) Element of K10(K11(NAT,K32(X)))

x is V7() V8() V9() V13() V14() ext-real V58() Element of NAT

(X,A1,A) . x is Element of K32(X)

n2 is V7() V8() V9() V13() V14() ext-real V58() Element of NAT

(X,A1,A) . n2 is Element of K32(X)

A1 . n2 is Element of K32(X)

A1 . x is Element of K32(X)

A \/ (A1 . n2) is Element of K10(X)

A \/ (A1 . x) is Element of K10(X)

X is set

K10(X) is V1() set

K32(X) is V1() Element of K10(K10(X))

K10(K10(X)) is V1() set

K11(NAT,K32(X)) is V1() set

K10(K11(NAT,K32(X))) is V1() set

A is Element of K10(X)

A1 is V1() V18() V21( NAT ) V22(K32(X)) Function-like V28( NAT ) V32( NAT ,K32(X)) Element of K10(K11(NAT,K32(X)))

(X,A1,A) is V1() V18() V21( NAT ) V22(K32(X)) Function-like V28( NAT ) V32( NAT ,K32(X)) Element of K10(K11(NAT,K32(X)))

x is V7() V8() V9() V13() V14() ext-real V58() Element of NAT

(X,A1,A) . x is Element of K32(X)

n2 is V7() V8() V9() V13() V14() ext-real V58() Element of NAT

(X,A1,A) . n2 is Element of K32(X)

A1 . x is Element of K32(X)

A1 . n2 is Element of K32(X)

A \/ (A1 . x) is Element of K10(X)

A \/ (A1 . n2) is Element of K10(X)

X is set

K10(X) is V1() set

K32(X) is V1() Element of K10(K10(X))

K10(K10(X)) is V1() set

K11(NAT,K32(X)) is V1() set

K10(K11(NAT,K32(X))) is V1() set

A is Element of K10(X)

A1 is V1() V18() V21( NAT ) V22(K32(X)) Function-like V28( NAT ) V32( NAT ,K32(X)) Element of K10(K11(NAT,K32(X)))

(X,A1,A) is V1() V18() V21( NAT ) V22(K32(X)) Function-like V28( NAT ) V32( NAT ,K32(X)) Element of K10(K11(NAT,K32(X)))

X is set

K10(X) is V1() set

K32(X) is V1() Element of K10(K10(X))

K10(K10(X)) is V1() set

K11(NAT,K32(X)) is V1() set

K10(K11(NAT,K32(X))) is V1() set

A is Element of K10(X)

A1 is V1() V18() V21( NAT ) V22(K32(X)) Function-like V28( NAT ) V32( NAT ,K32(X)) Element of K10(K11(NAT,K32(X)))

(X,A1,A) is V1() V18() V21( NAT ) V22(K32(X)) Function-like V28( NAT ) V32( NAT ,K32(X)) Element of K10(K11(NAT,K32(X)))

x is V7() V8() V9() V13() V14() ext-real V58() Element of NAT

(X,A1,A) . x is Element of K32(X)

n2 is V7() V8() V9() V13() V14() ext-real V58() Element of NAT

(X,A1,A) . n2 is Element of K32(X)

A1 . n2 is Element of K32(X)

A1 . x is Element of K32(X)

A \ (A1 . x) is Element of K10(X)

A \ (A1 . n2) is Element of K10(X)

X is set

K10(X) is V1() set

K32(X) is V1() Element of K10(K10(X))

K10(K10(X)) is V1() set

K11(NAT,K32(X)) is V1() set

K10(K11(NAT,K32(X))) is V1() set

A is Element of K10(X)

A1 is V1() V18() V21( NAT ) V22(K32(X)) Function-like V28( NAT ) V32( NAT ,K32(X)) Element of K10(K11(NAT,K32(X)))

(X,A1,A) is V1() V18() V21( NAT ) V22(K32(X)) Function-like V28( NAT ) V32( NAT ,K32(X)) Element of K10(K11(NAT,K32(X)))

x is V7() V8() V9() V13() V14() ext-real V58() Element of NAT

(X,A1,A) . x is Element of K32(X)

n2 is V7() V8() V9() V13() V14() ext-real V58() Element of NAT

(X,A1,A) . n2 is Element of K32(X)

A1 . x is Element of K32(X)

A1 . n2 is Element of K32(X)

A \ (A1 . n2) is Element of K10(X)

A \ (A1 . x) is Element of K10(X)

X is set

K10(X) is V1() set

K32(X) is V1() Element of K10(K10(X))

K10(K10(X)) is V1() set

K11(NAT,K32(X)) is V1() set

K10(K11(NAT,K32(X))) is V1() set

A is Element of K10(X)

A1 is V1() V18() V21( NAT ) V22(K32(X)) Function-like V28( NAT ) V32( NAT ,K32(X)) Element of K10(K11(NAT,K32(X)))

(X,A1,A) is V1() V18() V21( NAT ) V22(K32(X)) Function-like V28( NAT ) V32( NAT ,K32(X)) Element of K10(K11(NAT,K32(X)))

X is set

K10(X) is V1() set

K32(X) is V1() Element of K10(K10(X))

K10(K10(X)) is V1() set

K11(NAT,K32(X)) is V1() set

K10(K11(NAT,K32(X))) is V1() set

A is Element of K10(X)

A1 is V1() V18() V21( NAT ) V22(K32(X)) Function-like V28( NAT ) V32( NAT ,K32(X)) Element of K10(K11(NAT,K32(X)))

(X,A1,A) is V1() V18() V21( NAT ) V22(K32(X)) Function-like V28( NAT ) V32( NAT ,K32(X)) Element of K10(K11(NAT,K32(X)))

x is V7() V8() V9() V13() V14() ext-real V58() Element of NAT

(X,A1,A) . x is Element of K32(X)

n2 is V7() V8() V9() V13() V14() ext-real V58() Element of NAT

(X,A1,A) . n2 is Element of K32(X)

A1 . n2 is Element of K32(X)

A1 . x is Element of K32(X)

(A1 . n2) \ A is Element of K10(X)

(A1 . x) \ A is Element of K10(X)

X is set

K10(X) is V1() set

K32(X) is V1() Element of K10(K10(X))

K10(K10(X)) is V1() set

K11(NAT,K32(X)) is V1() set

K10(K11(NAT,K32(X))) is V1() set

A is Element of K10(X)

A1 is V1() V18() V21( NAT ) V22(K32(X)) Function-like V28( NAT ) V32( NAT ,K32(X)) Element of K10(K11(NAT,K32(X)))

(X,A1,A) is V1() V18() V21( NAT ) V22(K32(X)) Function-like V28( NAT ) V32( NAT ,K32(X)) Element of K10(K11(NAT,K32(X)))

x is V7() V8() V9() V13() V14() ext-real V58() Element of NAT

(X,A1,A) . x is Element of K32(X)

n2 is V7() V8() V9() V13() V14() ext-real V58() Element of NAT

(X,A1,A) . n2 is Element of K32(X)

A1 . x is Element of K32(X)

A1 . n2 is Element of K32(X)

(A1 . x) \ A is Element of K10(X)

(A1 . n2) \ A is Element of K10(X)

X is set

K10(X) is V1() set

K32(X) is V1() Element of K10(K10(X))

K10(K10(X)) is V1() set

K11(NAT,K32(X)) is V1() set

K10(K11(NAT,K32(X))) is V1() set

A is Element of K10(X)

A1 is V1() V18() V21( NAT ) V22(K32(X)) Function-like V28( NAT ) V32( NAT ,K32(X)) Element of K10(K11(NAT,K32(X)))

(X,A1,A) is V1() V18() V21( NAT ) V22(K32(X)) Function-like V28( NAT ) V32( NAT ,K32(X)) Element of K10(K11(NAT,K32(X)))

X is set

K10(X) is V1() set

K32(X) is V1() Element of K10(K10(X))

K10(K10(X)) is V1() set

K11(NAT,K32(X)) is V1() set

K10(K11(NAT,K32(X))) is V1() set

A is Element of K10(X)

A1 is V1() V18() V21( NAT ) V22(K32(X)) Function-like V28( NAT ) V32( NAT ,K32(X)) Element of K10(K11(NAT,K32(X)))

(X,A1,A) is V1() V18() V21( NAT ) V22(K32(X)) Function-like V28( NAT ) V32( NAT ,K32(X)) Element of K10(K11(NAT,K32(X)))

Intersection (X,A1,A) is Element of K10(X)

Intersection A1 is Element of K10(X)

A /\ (Intersection A1) is Element of K10(X)

x is set

n2 is V7() V8() V9() V13() V14() ext-real V58() Element of NAT

(X,A1,A) . n2 is Element of K32(X)

A1 . n2 is Element of K32(X)

A /\ (A1 . n2) is Element of K10(X)

x is set

n2 is V7() V8() V9() V13() V14() ext-real V58() Element of NAT

A1 . n2 is Element of K32(X)

A /\ (A1 . n2) is Element of K10(X)

(X,A1,A) . n2 is Element of K32(X)

X is set

K10(X) is V1() set

K32(X) is V1() Element of K10(K10(X))

K10(K10(X)) is V1() set

K11(NAT,K32(X)) is V1() set

K10(K11(NAT,K32(X))) is V1() set

A is Element of K10(X)

A1 is V1() V18() V21( NAT ) V22(K32(X)) Function-like V28( NAT ) V32( NAT ,K32(X)) Element of K10(K11(NAT,K32(X)))

(X,A1,A) is V1() V18() V21( NAT ) V22(K32(X)) Function-like V28( NAT ) V32( NAT ,K32(X)) Element of K10(K11(NAT,K32(X)))

Intersection (X,A1,A) is Element of K10(X)

Intersection A1 is Element of K10(X)

A \/ (Intersection A1) is Element of K10(X)

x is set

n2 is V7() V8() V9() V13() V14() ext-real V58() Element of NAT

(X,A1,A) . n2 is Element of K32(X)

A1 . n2 is Element of K32(X)

A \/ (A1 . n2) is Element of K10(X)

n2 is V7() V8() V9() V13() V14() ext-real V58() Element of NAT

A1 . n2 is Element of K32(X)

x is set

n2 is V7() V8() V9() V13() V14() ext-real V58() Element of NAT

A1 . n2 is Element of K32(X)

A \/ (A1 . n2) is Element of K10(X)

(X,A1,A) . n2 is Element of K32(X)

n2 is V7() V8() V9() V13() V14() ext-real V58() Element of NAT

A1 . n2 is Element of K32(X)

A \/ (A1 . n2) is Element of K10(X)

(X,A1,A) . n2 is Element of K32(X)

X is set

K10(X) is V1() set

K32(X) is V1() Element of K10(K10(X))

K10(K10(X)) is V1() set

K11(NAT,K32(X)) is V1() set

K10(K11(NAT,K32(X))) is V1() set

A is Element of K10(X)

A1 is V1() V18() V21( NAT ) V22(K32(X)) Function-like V28( NAT ) V32( NAT ,K32(X)) Element of K10(K11(NAT,K32(X)))

(X,A1,A) is V1() V18() V21( NAT ) V22(K32(X)) Function-like V28( NAT ) V32( NAT ,K32(X)) Element of K10(K11(NAT,K32(X)))

Intersection (X,A1,A) is Element of K10(X)

Intersection A1 is Element of K10(X)

A \ (Intersection A1) is Element of K10(X)

x is set

n2 is V7() V8() V9() V13() V14() ext-real V58() Element of NAT

(X,A1,A) . n2 is Element of K32(X)

A1 . n2 is Element of K32(X)

A \ (A1 . n2) is Element of K10(X)

0 is V7() V8() V9() V13() V14() ext-real V58() Element of NAT

the V1() V7() V8() V9() V11() V12() V13() V14() ext-real V58() set is V1() V7() V8() V9() V11() V12() V13() V14() ext-real V58() set

A1 . 0 is Element of K32(X)

X is set

K10(X) is V1() set

K32(X) is V1() Element of K10(K10(X))

K10(K10(X)) is V1() set

K11(NAT,K32(X)) is V1() set

K10(K11(NAT,K32(X))) is V1() set

A is Element of K10(X)

A1 is V1() V18() V21( NAT ) V22(K32(X)) Function-like V28( NAT ) V32( NAT ,K32(X)) Element of K10(K11(NAT,K32(X)))

(X,A1,A) is V1() V18() V21( NAT ) V22(K32(X)) Function-like V28( NAT ) V32( NAT ,K32(X)) Element of K10(K11(NAT,K32(X)))

Intersection (X,A1,A) is Element of K10(X)

Intersection A1 is Element of K10(X)

(Intersection A1) \ A is Element of K10(X)

x is set

n2 is V7() V8() V9() V13() V14() ext-real V58() Element of NAT

(X,A1,A) . n2 is Element of K32(X)

A1 . n2 is Element of K32(X)

(A1 . n2) \ A is Element of K10(X)

x is set

n2 is V7() V8() V9() V13() V14() ext-real V58() Element of NAT

A1 . n2 is Element of K32(X)

(A1 . n2) \ A is Element of K10(X)

(X,A1,A) . n2 is Element of K32(X)

X is set

K10(X) is V1() set

K32(X) is V1() Element of K10(K10(X))

K10(K10(X)) is V1() set

K11(NAT,K32(X)) is V1() set

K10(K11(NAT,K32(X))) is V1() set

A is Element of K10(X)

A1 is V1() V18() V21( NAT ) V22(K32(X)) Function-like V28( NAT ) V32( NAT ,K32(X)) Element of K10(K11(NAT,K32(X)))

(X,A1,A) is V1() V18() V21( NAT ) V22(K32(X)) Function-like V28( NAT ) V32( NAT ,K32(X)) Element of K10(K11(NAT,K32(X)))

Intersection (X,A1,A) is Element of K10(X)

Intersection A1 is Element of K10(X)

A \+\ (Intersection A1) is Element of K10(X)

K8(A,(Intersection A1)) is set

K8((Intersection A1),A) is set

K6(K8(A,(Intersection A1)),K8((Intersection A1),A)) is set

x is set

n2 is V7() V8() V9() V13() V14() ext-real V58() Element of NAT

(X,A1,A) . n2 is Element of K32(X)

A1 . n2 is Element of K32(X)

A \+\ (A1 . n2) is Element of K10(X)

K8(A,(A1 . n2)) is set

K8((A1 . n2),A) is set

K6(K8(A,(A1 . n2)),K8((A1 . n2),A)) is set

n2 is V7() V8() V9() V13() V14() ext-real V58() Element of NAT

A1 . n2 is Element of K32(X)

0 is V7() V8() V9() V13() V14() ext-real V58() Element of NAT

the V1() V7() V8() V9() V11() V12() V13() V14() ext-real V58() set is V1() V7() V8() V9() V11() V12() V13() V14() ext-real V58() set

A1 . 0 is Element of K32(X)

n2 is V7() V8() V9() V13() V14() ext-real V58() Element of NAT

A1 . n2 is Element of K32(X)

X is set

K10(X) is V1() set

K32(X) is V1() Element of K10(K10(X))

K10(K10(X)) is V1() set

K11(NAT,K32(X)) is V1() set

K10(K11(NAT,K32(X))) is V1() set

A is Element of K10(X)

A1 is V1() V18() V21( NAT ) V22(K32(X)) Function-like V28( NAT ) V32( NAT ,K32(X)) Element of K10(K11(NAT,K32(X)))

(X,A1,A) is V1() V18() V21( NAT ) V22(K32(X)) Function-like V28( NAT ) V32( NAT ,K32(X)) Element of K10(K11(NAT,K32(X)))

Union (X,A1,A) is Element of K10(X)

Union A1 is Element of K10(X)

A /\ (Union A1) is Element of K10(X)

x is set

n2 is V7() V8() V9() V13() V14() ext-real V58() Element of NAT

(X,A1,A) . n2 is Element of K32(X)

A1 . n2 is Element of K32(X)

A /\ (A1 . n2) is Element of K10(X)

x is set

n2 is V7() V8() V9() V13() V14() ext-real V58() Element of NAT

A1 . n2 is Element of K32(X)

A /\ (A1 . n2) is Element of K10(X)

(X,A1,A) . n2 is Element of K32(X)

X is set

K10(X) is V1() set

K32(X) is V1() Element of K10(K10(X))

K10(K10(X)) is V1() set

K11(NAT,K32(X)) is V1() set

K10(K11(NAT,K32(X))) is V1() set

A is Element of K10(X)

A1 is V1() V18() V21( NAT ) V22(K32(X)) Function-like V28( NAT ) V32( NAT ,K32(X)) Element of K10(K11(NAT,K32(X)))

(X,A1,A) is V1() V18() V21( NAT ) V22(K32(X)) Function-like V28( NAT ) V32( NAT ,K32(X)) Element of K10(K11(NAT,K32(X)))

Union (X,A1,A) is Element of K10(X)

Union A1 is Element of K10(X)

A \/ (Union A1) is Element of K10(X)

x is set

n2 is V7() V8() V9() V13() V14() ext-real V58() Element of NAT

(X,A1,A) . n2 is Element of K32(X)

A1 . n2 is Element of K32(X)

A \/ (A1 . n2) is Element of K10(X)

n2 is V7() V8() V9() V13() V14() ext-real V58() Element of NAT

A1 . n2 is Element of K32(X)

n2 is V7() V8() V9() V13() V14() ext-real V58() Element of NAT

A1 . n2 is Element of K32(X)

x is set

1 is V7() V8() V9() V13() V14() ext-real V58() Element of NAT

A1 . 1 is Element of K32(X)

A \/ (A1 . 1) is Element of K10(X)

(X,A1,A) . 1 is Element of K32(X)

n2 is V7() V8() V9() V13() V14() ext-real V58() Element of NAT

A1 . n2 is Element of K32(X)

A \/ (A1 . n2) is Element of K10(X)

(X,A1,A) . n2 is Element of K32(X)

X is set

K10(X) is V1() set

K32(X) is V1() Element of K10(K10(X))

K10(K10(X)) is V1() set

K11(NAT,K32(X)) is V1() set

K10(K11(NAT,K32(X))) is V1() set

A is Element of K10(X)

A1 is V1() V18() V21( NAT ) V22(K32(X)) Function-like V28( NAT ) V32( NAT ,K32(X)) Element of K10(K11(NAT,K32(X)))

Union A1 is Element of K10(X)

A \ (Union A1) is Element of K10(X)

(X,A1,A) is V1() V18() V21( NAT ) V22(K32(X)) Function-like V28( NAT ) V32( NAT ,K32(X)) Element of K10(K11(NAT,K32(X)))

Union (X,A1,A) is Element of K10(X)

x is set

n2 is V7() V8() V9() V13() V14() ext-real V58() Element of NAT

A1 . n2 is Element of K32(X)

A \ (A1 . n2) is Element of K10(X)

(X,A1,A) . n2 is Element of K32(X)

1 is V7() V8() V9() V13() V14() ext-real V58() Element of NAT

(X,A1,A) . 1 is Element of K32(X)

X is set

K10(X) is V1() set

K32(X) is V1() Element of K10(K10(X))

K10(K10(X)) is V1() set

K11(NAT,K32(X)) is V1() set

K10(K11(NAT,K32(X))) is V1() set

A is Element of K10(X)

A1 is V1() V18() V21( NAT ) V22(K32(X)) Function-like V28( NAT ) V32( NAT ,K32(X)) Element of K10(K11(NAT,K32(X)))

(X,A1,A) is V1() V18() V21( NAT ) V22(K32(X)) Function-like V28( NAT ) V32( NAT ,K32(X)) Element of K10(K11(NAT,K32(X)))

Union (X,A1,A) is Element of K10(X)

Union A1 is Element of K10(X)

(Union A1) \ A is Element of K10(X)

x is set

n2 is V7() V8() V9() V13() V14() ext-real V58() Element of NAT

(X,A1,A) . n2 is Element of K32(X)

A1 . n2 is Element of K32(X)

(A1 . n2) \ A is Element of K10(X)

n2 is V7() V8() V9() V13() V14() ext-real V58() Element of NAT

A1 . n2 is Element of K32(X)

n2 is V7() V8() V9() V13() V14() ext-real V58() Element of NAT

A1 . n2 is Element of K32(X)

x is set

n2 is V7() V8() V9() V13() V14() ext-real V58() Element of NAT

A1 . n2 is Element of K32(X)

(A1 . n2) \ A is Element of K10(X)

(X,A1,A) . n2 is Element of K32(X)

n2 is V7() V8() V9() V13() V14() ext-real V58() Element of NAT

(X,A1,A) . n2 is Element of K32(X)

X is set

K10(X) is V1() set

K32(X) is V1() Element of K10(K10(X))

K10(K10(X)) is V1() set

K11(NAT,K32(X)) is V1() set

K10(K11(NAT,K32(X))) is V1() set

A is Element of K10(X)

A1 is V1() V18() V21( NAT ) V22(K32(X)) Function-like V28( NAT ) V32( NAT ,K32(X)) Element of K10(K11(NAT,K32(X)))

Union A1 is Element of K10(X)

A \+\ (Union A1) is Element of K10(X)

K8(A,(Union A1)) is set

K8((Union A1),A) is set

K6(K8(A,(Union A1)),K8((Union A1),A)) is set

(X,A1,A) is V1() V18() V21( NAT ) V22(K32(X)) Function-like V28( NAT ) V32( NAT ,K32(X)) Element of K10(K11(NAT,K32(X)))

Union (X,A1,A) is Element of K10(X)

x is set

0 is V7() V8() V9() V13() V14() ext-real V58() Element of NAT

the V1() V7() V8() V9() V11() V12() V13() V14() ext-real V58() set is V1() V7() V8() V9() V11() V12() V13() V14() ext-real V58() set

A1 . 0 is Element of K32(X)

A \+\ (A1 . 0) is Element of K10(X)

K8(A,(A1 . 0)) is set

K8((A1 . 0),A) is set

K6(K8(A,(A1 . 0)),K8((A1 . 0),A)) is set

(X,A1,A) . 0 is Element of K32(X)

n2 is V7() V8() V9() V13() V14() ext-real V58() Element of NAT

A1 . n2 is Element of K32(X)

A \+\ (A1 . n2) is Element of K10(X)

K8(A,(A1