:: 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₁) where b₁ is V7() V8() V9() V13() V14() ext-real V58() Element of NAT : X <= b₁ } is set
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₁) where b₁ is V7() V8() V9() V13() V14() ext-real V58() Element of NAT : X <= b₁ } is set
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