:: 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 . n2)) is set
K8((A1 . n2),A) is set
K6(K8(A,(A1 . n2)),K8((A1 . n2),A)) is set
(X,A1,A) . n2 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)))
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)
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)))
inferior_setsequence (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)))
(inferior_setsequence (A,A1,x)) . X is Element of K32(A)
inferior_setsequence x 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 x) . X is Element of K32(A)
((inferior_setsequence A1) . X) /\ ((inferior_setsequence x) . X) is Element of K10(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)))
Intersection ((A,A1,x) ^\ X) is Element of K10(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 ^\ 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)))
Intersection (A,(A1 ^\ X),(x ^\ X)) is Element of K10(A)
Intersection (A1 ^\ X) is Element of K10(A)
Intersection (x ^\ X) is Element of K10(A)
(Intersection (A1 ^\ X)) /\ (Intersection (x ^\ X)) is Element of K10(A)
((inferior_setsequence A1) . X) /\ (Intersection (x ^\ X)) is Element of K10(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)))
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)
x 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 x 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 x) . X is Element of K32(A)
((inferior_setsequence A1) . X) \/ ((inferior_setsequence x) . X) is Element of K10(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)))
inferior_setsequence (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)))
(inferior_setsequence (A,A1,x)) . 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)))
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)))
Intersection (A,(A1 ^\ X),(x ^\ X)) is Element of K10(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)))
Intersection ((A,A1,x) ^\ X) is Element of K10(A)
Intersection (A1 ^\ X) is Element of K10(A)
(Intersection (A1 ^\ X)) \/ ((inferior_setsequence x) . X) is Element of K10(A)
Intersection (x ^\ X) is Element of K10(A)
(Intersection (A1 ^\ X)) \/ (Intersection (x ^\ X)) is Element of K10(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)))
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)
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)))
inferior_setsequence (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)))
(inferior_setsequence (A,A1,x)) . X is Element of K32(A)
inferior_setsequence x 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 x) . X is Element of K32(A)
((inferior_setsequence A1) . X) \ ((inferior_setsequence x) . X) is Element of K10(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)))
Intersection ((A,A1,x) ^\ X) is Element of K10(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 ^\ 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)))
Intersection (A,(A1 ^\ X),(x ^\ X)) is Element of K10(A)
Intersection (A1 ^\ X) is Element of K10(A)
Intersection (x ^\ X) is Element of K10(A)
(Intersection (A1 ^\ X)) \ (Intersection (x ^\ X)) is Element of K10(A)
((inferior_setsequence A1) . X) \ (Intersection (x ^\ X)) is Element of K10(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)))
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)
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)))
superior_setsequence (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)))
(superior_setsequence (A,A1,x)) . X is Element of K32(A)
superior_setsequence x 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 x) . X is Element of K32(A)
((superior_setsequence A1) . X) /\ ((superior_setsequence x) . X) is Element of K10(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)))
Union ((A,A1,x) ^\ X) is Element of K10(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 ^\ 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)))
Union (A,(A1 ^\ X),(x ^\ X)) is Element of K10(A)
Union (A1 ^\ X) is Element of K10(A)
Union (x ^\ X) is Element of K10(A)
(Union (A1 ^\ X)) /\ (Union (x ^\ X)) is Element of K10(A)
((superior_setsequence A1) . X) /\ (Union (x ^\ X)) is Element of K10(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)))
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)
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)))
superior_setsequence (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)))
(superior_setsequence (A,A1,x)) . X is Element of K32(A)
superior_setsequence x 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 x) . X is Element of K32(A)
((superior_setsequence A1) . X) \/ ((superior_setsequence x) . X) is Element of K10(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)))
Union ((A,A1,x) ^\ X) is Element of K10(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 ^\ 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)))
Union (A,(A1 ^\ X),(x ^\ X)) is Element of K10(A)
Union (A1 ^\ X) is Element of K10(A)
Union (x ^\ X) is Element of K10(A)
(Union (A1 ^\ X)) \/ (Union (x ^\ X)) is Element of K10(A)
((superior_setsequence A1) . X) \/ (Union (x ^\ X)) is Element of K10(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)))
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)
x 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 x 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 x) . X is Element of K32(A)
((superior_setsequence A1) . X) \ ((superior_setsequence x) . X) is Element of K10(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)))
superior_setsequence (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)))
(superior_setsequence (A,A1,x)) . 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)
(Union (A1 ^\ X)) \ ((superior_setsequence x) . X) is Element of K10(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)))
Union (x ^\ X) is Element of K10(A)
(Union (A1 ^\ X)) \ (Union (x ^\ X)) is Element of K10(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)))
Union (A,(A1 ^\ X),(x ^\ X)) is Element of K10(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)))
Union ((A,A1,x) ^\ X) is Element of K10(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)))
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)
x 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 x 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 x) . X is Element of K32(A)
((superior_setsequence A1) . X) \+\ ((superior_setsequence x) . X) is Element of K10(A)
K8(((superior_setsequence A1) . X),((superior_setsequence x) . X)) is set
K8(((superior_setsequence x) . X),((superior_setsequence A1) . X)) is set
K6(K8(((superior_setsequence A1) . X),((superior_setsequence x) . X)),K8(((superior_setsequence x) . X),((superior_setsequence A1) . X))) is set
(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)))
superior_setsequence (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)))
(superior_setsequence (A,A1,x)) . 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)
(Union (A1 ^\ X)) \+\ ((superior_setsequence x) . X) is Element of K10(A)
K8((Union (A1 ^\ X)),((superior_setsequence x) . X)) is set
K8(((superior_setsequence x) . X),(Union (A1 ^\ X))) is set
K6(K8((Union (A1 ^\ X)),((superior_setsequence x) . X)),K8(((superior_setsequence x) . X),(Union (A1 ^\ X)))) is set
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)))
Union (x ^\ X) is Element of K10(A)
(Union (A1 ^\ X)) \+\ (Union (x ^\ X)) is Element of K10(A)
K8((Union (A1 ^\ X)),(Union (x ^\ X))) is set
K8((Union (x ^\ X)),(Union (A1 ^\ X))) is set
K6(K8((Union (A1 ^\ X)),(Union (x ^\ X))),K8((Union (x ^\ X)),(Union (A1 ^\ X)))) is set
(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)))
Union (A,(A1 ^\ X),(x ^\ X)) is Element of K10(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)))
Union ((A,A1,x) ^\ X) is Element of K10(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)))
inferior_setsequence (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)))
(inferior_setsequence (A,x,A1)) . X is Element of K32(A)
inferior_setsequence x 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 x) . X is Element of K32(A)
A1 /\ ((inferior_setsequence x) . X) is Element of K10(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)))
Intersection ((A,x,A1) ^\ X) is Element of K10(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)))
Intersection (A,(x ^\ X),A1) is Element of K10(A)
Intersection (x ^\ X) is Element of K10(A)
A1 /\ (Intersection (x ^\ X)) is Element of K10(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)))
inferior_setsequence (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)))
(inferior_setsequence (A,x,A1)) . X is Element of K32(A)
inferior_setsequence x 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 x) . X is Element of K32(A)
A1 \/ ((inferior_setsequence x) . X) is Element of K10(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)))
Intersection ((A,x,A1) ^\ X) is Element of K10(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)))
Intersection (A,(x ^\ X),A1) is Element of K10(A)
Intersection (x ^\ X) is Element of K10(A)
A1 \/ (Intersection (x ^\ X)) is Element of K10(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)))
inferior_setsequence (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)))
(inferior_setsequence (A,x,A1)) . X is Element of K32(A)
inferior_setsequence x 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 x) . X is Element of K32(A)
A1 \ ((inferior_setsequence x) . X) is Element of K10(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)))
Intersection ((A,x,A1) ^\ X) is Element of K10(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)))
Intersection (A,(x ^\ X),A1) is Element of K10(A)
Intersection (x ^\ X) is Element of K10(A)
A1 \ (Intersection (x ^\ X)) is Element of K10(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)))
inferior_setsequence (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)))
(inferior_setsequence (A,x,A1)) . X is Element of K32(A)
inferior_setsequence x 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 x) . X is Element of K32(A)
((inferior_setsequence x) . X) \ A1 is Element of K10(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)))
Intersection ((A,x,A1) ^\ X) is Element of K10(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)))
Intersection (A,(x ^\ X),A1) is Element of K10(A)
Intersection (x ^\ X) is Element of K10(A)
(Intersection (x ^\ X)) \ A1 is Element of K10(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)))
inferior_setsequence (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)))
(inferior_setsequence (A,x,A1)) . X is Element of K32(A)
inferior_setsequence x 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 x) . X is Element of K32(A)
A1 \+\ ((inferior_setsequence x) . X) is Element of K10(A)
K8(A1,((inferior_setsequence x) . X)) is set
K8(((inferior_setsequence x) . X),A1) is set
K6(K8(A1,((inferior_setsequence x) . X)),K8(((inferior_setsequence x) . X),A1)) is set
(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)))
Intersection ((A,x,A1) ^\ X) is Element of K10(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)))
Intersection (A,(x ^\ X),A1) is Element of K10(A)
Intersection (x ^\ X) is Element of K10(A)
A1 \+\ (Intersection (x ^\ X)) is Element of K10(A)
K8(A1,(Intersection (x ^\ X))) is set
K8((Intersection (x ^\ X)),A1) is set
K6(K8(A1,(Intersection (x ^\ X))),K8((Intersection (x ^\ X)),A1)) is set
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)))
superior_setsequence (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)))
(superior_setsequence (A,x,A1)) . X is Element of K32(A)
superior_setsequence x 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 x) . X is Element of K32(A)
A1 /\ ((superior_setsequence x) . X) is Element of K10(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)))
Union ((A,x,A1) ^\ X) is Element of K10(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)))
Union (A,(x ^\ X),A1) is Element of K10(A)
Union (x ^\ X) is Element of K10(A)
A1 /\ (Union (x ^\ X)) is Element of K10(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)))
superior_setsequence (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)))
(superior_setsequence (A,x,A1)) . X is Element of K32(A)
superior_setsequence x 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 x) . X is Element of K32(A)
A1 \/ ((superior_setsequence x) . X) is Element of K10(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)))
Union ((A,x,A1) ^\ X) is Element of K10(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)))
Union (A,(x ^\ X),A1) is Element of K10(A)
Union (x ^\ X) is Element of K10(A)
A1 \/ (Union (x ^\ X)) is Element of K10(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)))
superior_setsequence x 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 x) . X is Element of K32(A)
A1 \ ((superior_setsequence x) . X) is Element of K10(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)))
superior_setsequence (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)))
(superior_setsequence (A,x,A1)) . X is Element of 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)))
Union (x ^\ X) is Element of K10(A)
A1 \ (Union (x ^\ X)) is Element of K10(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)))
Union (A,(x ^\ X),A1) is Element of K10(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)))
Union ((A,x,A1) ^\ X) is Element of K10(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)))
superior_setsequence (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)))
(superior_setsequence (A,x,A1)) . X is Element of K32(A)
superior_setsequence x 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 x) . X is Element of K32(A)
((superior_setsequence x) . X) \ A1 is Element of K10(A)
n2 is V1() V18() V21( NAT ) V22(K32(A)) Function-like V28( NAT ) V32( NAT ,K32(A)) Element of K10(K11(NAT,K32(A)))
n2 . X is Element of K32(A)
(n2 . X) \ A1 is Element of K10(A)
k1 is V1() V18() V21( NAT ) V22(K32(A)) Function-like V28( NAT ) V32( NAT ,K32(A)) Element of K10(K11(NAT,K32(A)))
k1 . X is Element of K32(A)
k is set
n is V7() V8() V9() V13() V14() ext-real V58() Element of NAT
X + n is V7() V8() V9() V13() V14() ext-real V58() Element of NAT
x . (X + n) is Element of K32(A)
(x . (X + n)) \ A1 is Element of K10(A)
(A,x,A1) . (X + n) is Element of K32(A)
n is V7() V8() V9() V13() V14() ext-real V58() Element of NAT
X + n is V7() V8() V9() V13() V14() ext-real V58() Element of NAT
(A,x,A1) . (X + n) is Element of K32(A)
k is set
n is V7() V8() V9() V13() V14() ext-real V58() Element of NAT
X + n is V7() V8() V9() V13() V14() ext-real V58() Element of NAT
(A,x,A1) . (X + n) is Element of K32(A)
x . (X + n) is Element of K32(A)
(x . (X + n)) \ A1 is Element of K10(A)
n is V7() V8() V9() V13() V14() ext-real V58() Element of NAT
X + n is V7() V8() V9() V13() V14() ext-real V58() Element of NAT
x . (X + n) is Element of K32(A)
n is V7() V8() V9() V13() V14() ext-real V58() Element of NAT
X + n is V7() V8() V9() V13() V14() ext-real V58() Element of NAT
x . (X + n) 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)))
superior_setsequence x 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 x) . X is Element of K32(A)
A1 \+\ ((superior_setsequence x) . X) is Element of K10(A)
K8(A1,((superior_setsequence x) . X)) is set
K8(((superior_setsequence x) . X),A1) is set
K6(K8(A1,((superior_setsequence x) . X)),K8(((superior_setsequence x) . X),A1)) is set
(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)))
superior_setsequence (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)))
(superior_setsequence (A,x,A1)) . X is Element of 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)))
Union (x ^\ X) is Element of K10(A)
A1 \+\ (Union (x ^\ X)) is Element of K10(A)
K8(A1,(Union (x ^\ X))) is set
K8((Union (x ^\ X)),A1) is set
K6(K8(A1,(Union (x ^\ X))),K8((Union (x ^\ X)),A1)) is set
(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)))
Union (A,(x ^\ X),A1) is Element of K10(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)))
Union ((A,x,A1) ^\ X) is Element of K10(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)))
lim_inf 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)))
lim_inf (X,A,A1) is Element of K10(X)
lim_inf A1 is Element of K10(X)
(lim_inf A) /\ (lim_inf A1) is Element of K10(X)
x is V7() V8() V9() V13() V14() ext-real V58() Element of NAT
(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)
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)))
lim_inf 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)))
lim_inf A1 is Element of K10(X)
(lim_inf A) \/ (lim_inf 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)))
lim_inf (X,A,A1) is Element of K10(X)
x is V7() V8() V9() V13() V14() ext-real V58() Element of NAT
(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)
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)))
lim_inf 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)))
lim_inf (X,A,A1) is Element of K10(X)
lim_inf A1 is Element of K10(X)
(lim_inf A) \ (lim_inf A1) is Element of K10(X)
x is set
n2 is V7() V8() V9() V13() V14() ext-real V58() Element of NAT
k1 is V7() V8() V9() V13() V14() ext-real V58() Element of NAT
n2 + k1 is V7() V8() V9() V13() V14() ext-real V58() Element of NAT
(X,A,A1) . (n2 + k1) is Element of K32(X)
A . (n2 + k1) is Element of K32(X)
A1 . (n2 + k1) is Element of K32(X)
(A . (n2 + k1)) \ (A1 . (n2 + k1)) is Element of K10(X)
k1 is V7() V8() V9() V13() V14() ext-real V58() Element of NAT
k1 + n2 is V7() V8() V9() V13() V14() ext-real V58() Element of NAT
A1 . (k1 + 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)))
lim_inf 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)))
lim_inf (X,A,A1) is Element of K10(X)
lim_inf A1 is Element of K10(X)
(lim_inf A) \/ (lim_inf A1) 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)))
lim_inf x is Element of K10(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)))
(X,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)))
lim_inf (X,x,n2) is Element of K10(X)
lim_inf n2 is Element of K10(X)
(lim_inf x) \/ (lim_inf n2) is Element of K10(X)
k1 is set
k is V7() V8() V9() V13() V14() ext-real V58() Element of NAT
n is V7() V8() V9() V13() V14() ext-real V58() Element of NAT
k + n is V7() V8() V9() V13() V14() ext-real V58() Element of NAT
(X,x,n2) . (k + n) is Element of K32(X)
x . (k + n) is Element of K32(X)
n2 . (k + n) is Element of K32(X)
(x . (k + n)) \/ (n2 . (k + n)) is Element of K10(X)
lim_sup x is Element of K10(X)
n is V7() V8() V9() V13() V14() ext-real V58() Element of NAT
k + n is V7() V8() V9() V13() V14() ext-real V58() Element of NAT
k1 is V7() V8() V9() V13() V14() ext-real V58() Element of NAT
(k + n) + k1 is V7() V8() V9() V13() V14() ext-real V58() Element of NAT
n2 . ((k + n) + k1) is Element of K32(X)
k + k1 is V7() V8() V9() V13() V14() ext-real V58() Element of NAT
n + (k + k1) is V7() V8() V9() V13() V14() ext-real V58() Element of NAT
x . (n + (k + k1)) is Element of K32(X)
n + k1 is V7() V8() V9() V13() V14() ext-real V58() Element of NAT
k + (n + k1) is V7() V8() V9() V13() V14() ext-real V58() Element of NAT
x . (k + (n + k1)) 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)))
lim_inf 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)))
lim_inf (X,A1,A) is Element of K10(X)
lim_inf A1 is Element of K10(X)
(lim_inf A1) \ (lim_inf A) is Element of K10(X)
x is set
n2 is V7() V8() V9() V13() V14() ext-real V58() Element of NAT
lim_sup A is Element of K10(X)
k1 is V7() V8() V9() V13() V14() ext-real V58() Element of NAT
k is V7() V8() V9() V13() V14() ext-real V58() Element of NAT
k1 + k is V7() V8() V9() V13() V14() ext-real V58() Element of NAT
n2 + (k1 + k) is V7() V8() V9() V13() V14() ext-real V58() Element of NAT
A1 . (n2 + (k1 + k)) is Element of K32(X)
n2 + k is V7() V8() V9() V13() V14() ext-real V58() Element of NAT
k1 + (n2 + k) is V7() V8() V9() V13() V14() ext-real V58() Element of NAT
A . (k1 + (n2 + k)) is Element of K32(X)
n2 + k1 is V7() V8() V9() V13() V14() ext-real V58() Element of NAT
(n2 + k1) + k is V7() V8() V9() V13() V14() ext-real V58() Element of NAT
A1 . ((n2 + k1) + k) is Element of K32(X)
A . ((n2 + k1) + k) is Element of K32(X)
(A1 . ((n2 + k1) + k)) \ (A . ((n2 + k1) + k)) is Element of K10(X)
(X,A1,A) . ((n2 + k1) + k) 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)))
lim_inf 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)))
lim_inf (X,A,A1) is Element of K10(X)
lim_inf A1 is Element of K10(X)
(lim_inf A) \+\ (lim_inf A1) is Element of K10(X)
K8((lim_inf A),(lim_inf A1)) is set
K8((lim_inf A1),(lim_inf A)) is set
K6(K8((lim_inf A),(lim_inf A1)),K8((lim_inf A1),(lim_inf A))) is set
x is V1() V18() V21( NAT ) V22(K32(X)) Function-like V28( NAT ) V32( NAT ,K32(X)) Element of K10(K11(NAT,K32(X)))
lim_inf x is Element of K10(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)))
(X,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)))
lim_inf (X,x,n2) is Element of K10(X)
lim_inf n2 is Element of K10(X)
(lim_inf x) \+\ (lim_inf n2) is Element of K10(X)
K8((lim_inf x),(lim_inf n2)) is set
K8((lim_inf n2),(lim_inf x)) is set
K6(K8((lim_inf x),(lim_inf n2)),K8((lim_inf n2),(lim_inf x))) is set
k1 is set
k is V7() V8() V9() V13() V14() ext-real V58() Element of NAT
n is V7() V8() V9() V13() V14() ext-real V58() Element of NAT
k + n is V7() V8() V9() V13() V14() ext-real V58() Element of NAT
(X,x,n2) . (k + n) is Element of K32(X)
x . (k + n) is Element of K32(X)
n2 . (k + n) is Element of K32(X)
(x . (k + n)) \+\ (n2 . (k + n)) is Element of K10(X)
K8((x . (k + n)),(n2 . (k + n))) is set
K8((n2 . (k + n)),(x . (k + n))) is set
K6(K8((x . (k + n)),(n2 . (k + n))),K8((n2 . (k + n)),(x . (k + n)))) is set
lim_sup x is Element of K10(X)
n is V7() V8() V9() V13() V14() ext-real V58() Element of NAT
k + n is V7() V8() V9() V13() V14() ext-real V58() Element of NAT
k1 is V7() V8() V9() V13() V14() ext-real V58() Element of NAT
(k + n) + k1 is V7() V8() V9() V13() V14() ext-real V58() Element of NAT
n2 . ((k + n) + k1) is Element of K32(X)
n + k1 is V7() V8() V9() V13() V14() ext-real V58() Element of NAT
k + (n + k1) is V7() V8() V9() V13() V14() ext-real V58() Element of NAT
x . (k + (n + k1)) is Element of K32(X)
n2 . (k + (n + k1)) is Element of K32(X)
k + k1 is V7() V8() V9() V13() V14() ext-real V58() Element of NAT
n + (k + k1) is V7() V8() V9() V13() V14() ext-real V58() Element of NAT
x . (n + (k + k1)) is Element of K32(X)
n is V7() V8() V9() V13() V14() ext-real V58() Element of NAT
k1 is V7() V8() V9() V13() V14() ext-real V58() Element of NAT
k1 + n is V7() V8() V9() V13() V14() ext-real V58() Element of NAT
k + (k1 + n) is V7() V8() V9() V13() V14() ext-real V58() Element of NAT
x . (k + (k1 + n)) is Element of K32(X)
n2 . (k + (k1 + n)) is Element of K32(X)
k + k1 is V7() V8() V9() V13() V14() ext-real V58() Element of NAT
n + (k + k1) is V7() V8() V9() V13() V14() ext-real V58() Element of NAT
n2 . (n + (k + k1)) is Element of K32(X)
k + n is V7() V8() V9() V13() V14() ext-real V58() Element of NAT
k1 + (k + n) is V7() V8() V9() V13() V14() ext-real V58() Element of NAT
x . (k1 + (k + n)) 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)))
lim_inf 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)))
lim_inf (X,A,A1) is Element of K10(X)
lim_inf A1 is Element of K10(X)
(lim_inf A) \+\ (lim_inf A1) is Element of K10(X)
K8((lim_inf A),(lim_inf A1)) is set
K8((lim_inf A1),(lim_inf A)) is set
K6(K8((lim_inf A),(lim_inf A1)),K8((lim_inf A1),(lim_inf A))) is set
x is set
lim_sup A1 is Element of K10(X)
n2 is V7() V8() V9() V13() V14() ext-real V58() Element of NAT
k1 is V7() V8() V9() V13() V14() ext-real V58() Element of NAT
k is V7() V8() V9() V13() V14() ext-real V58() Element of NAT
n2 + k is V7() V8() V9() V13() V14() ext-real V58() Element of NAT
k1 + (n2 + k) is V7() V8() V9() V13() V14() ext-real V58() Element of NAT
A . (k1 + (n2 + k)) is Element of K32(X)
k1 + k is V7() V8() V9() V13() V14() ext-real V58() Element of NAT
n2 + (k1 + k) is V7() V8() V9() V13() V14() ext-real V58() Element of NAT
A1 . (n2 + (k1 + k)) is Element of K32(X)
k1 + n2 is V7() V8() V9() V13() V14() ext-real V58() Element of NAT
(k1 + n2) + k is V7() V8() V9() V13() V14() ext-real V58() Element of NAT
A . ((k1 + n2) + k) is Element of K32(X)
A1 . ((k1 + n2) + k) is Element of K32(X)
(A . ((k1 + n2) + k)) \+\ (A1 . ((k1 + n2) + k)) is Element of K10(X)
K8((A . ((k1 + n2) + k)),(A1 . ((k1 + n2) + k))) is set
K8((A1 . ((k1 + n2) + k)),(A . ((k1 + n2) + k))) is set
K6(K8((A . ((k1 + n2) + k)),(A1 . ((k1 + n2) + k))),K8((A1 . ((k1 + n2) + k)),(A . ((k1 + n2) + k)))) is set
(X,A,A1) . ((k1 + n2) + k) is Element of K32(X)
lim_sup A is Element of K10(X)
n2 is V7() V8() V9() V13() V14() ext-real V58() Element of NAT
k1 is V7() V8() V9() V13() V14() ext-real V58() Element of NAT
k is V7() V8() V9() V13() V14() ext-real V58() Element of NAT
k1 + k is V7() V8() V9() V13() V14() ext-real V58() Element of NAT
n2 + (k1 + k) is V7() V8() V9() V13() V14() ext-real V58() Element of NAT
A . (n2 + (k1 + k)) is Element of K32(X)
n2 + k is V7() V8() V9() V13() V14() ext-real V58() Element of NAT
k1 + (n2 + k) is V7() V8() V9() V13() V14() ext-real V58() Element of NAT
A1 . (k1 + (n2 + k)) is Element of K32(X)
n2 + k1 is V7() V8() V9() V13() V14() ext-real V58() Element of NAT
(n2 + k1) + k is V7() V8() V9() V13() V14() ext-real V58() Element of NAT
A . ((n2 + k1) + k) is Element of K32(X)
A1 . ((n2 + k1) + k) is Element of K32(X)
(A . ((n2 + k1) + k)) \+\ (A1 . ((n2 + k1) + k)) is Element of K10(X)
K8((A . ((n2 + k1) + k)),(A1 . ((n2 + k1) + k))) is set
K8((A1 . ((n2 + k1) + k)),(A . ((n2 + k1) + k))) is set
K6(K8((A . ((n2 + k1) + k)),(A1 . ((n2 + k1) + k))),K8((A1 . ((n2 + k1) + k)),(A . ((n2 + k1) + k)))) is set
(X,A,A1) . ((n2 + k1) + k) 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)))
lim_sup 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)))
lim_sup (X,A,A1) is Element of K10(X)
lim_sup A1 is Element of K10(X)
(lim_sup A) /\ (lim_sup A1) is Element of K10(X)
x is V7() V8() V9() V13() V14() ext-real V58() Element of NAT
(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)
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)))
lim_sup 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)))
lim_sup (X,A,A1) is Element of K10(X)
lim_sup A1 is Element of K10(X)
(lim_sup A) \/ (lim_sup A1) is Element of K10(X)
x is V7() V8() V9() V13() V14() ext-real V58() Element of NAT
(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)
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)))
lim_sup 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)))
lim_sup A1 is Element of K10(X)
(lim_sup A) \ (lim_sup 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)))
lim_sup (X,A,A1) is Element of K10(X)
x is set
n2 is V7() V8() V9() V13() V14() ext-real V58() Element of NAT
k1 is V7() V8() V9() V13() V14() ext-real V58() Element of NAT
k is V7() V8() V9() V13() V14() ext-real V58() Element of NAT
k1 + k is V7() V8() V9() V13() V14() ext-real V58() Element of NAT
(X,A,A1) . (k1 + k) is Element of K32(X)
A . (k1 + k) is Element of K32(X)
A1 . (k1 + k) is Element of K32(X)
(A . (k1 + k)) \ (A1 . (k1 + k)) is Element of K10(X)
n2 + k1 is V7() V8() V9() V13() V14() ext-real V58() Element of NAT
k is V7() V8() V9() V13() V14() ext-real V58() Element of NAT
(n2 + k1) + k is V7() V8() V9() V13() V14() ext-real V58() Element of NAT
A . ((n2 + k1) + k) is Element of K32(X)
k + n2 is V7() V8() V9() V13() V14() ext-real V58() Element of NAT
k1 + (k + n2) is V7() V8() V9() V13() V14() ext-real V58() Element of NAT
A . (k1 + (k + n2)) is Element of K32(X)
k1 + k is V7() V8() V9() V13() V14() ext-real V58() Element of NAT
n2 + (k1 + k) is V7() V8() V9() V13() V14() ext-real V58() Element of NAT
A1 . (n2 + (k1 + k)) 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)))
lim_sup 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)))
lim_sup A1 is Element of K10(X)
(lim_sup A) \+\ (lim_sup A1) is Element of K10(X)
K8((lim_sup A),(lim_sup A1)) is set
K8((lim_sup A1),(lim_sup A)) is set
K6(K8((lim_sup A),(lim_sup A1)),K8((lim_sup A1),(lim_sup 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)))
lim_sup (X,A,A1) is Element of K10(X)
x is set
n2 is V1() V18() V21( NAT ) V22(K32(X)) Function-like V28( NAT ) V32( NAT ,K32(X)) Element of K10(K11(NAT,K32(X)))
lim_sup n2 is Element of K10(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)))
lim_sup k1 is Element of K10(X)
(X,n2,k1) is V1() V18() V21( NAT ) V22(K32(X)) Function-like V28( NAT ) V32( NAT ,K32(X)) Element of K10(K11(NAT,K32(X)))
lim_sup (X,n2,k1) is Element of K10(X)
k is V7() V8() V9() V13() V14() ext-real V58() Element of NAT
n is V7() V8() V9() V13() V14() ext-real V58() Element of NAT
n + k is V7() V8() V9() V13() V14() ext-real V58() Element of NAT
k1 is V7() V8() V9() V13() V14() ext-real V58() Element of NAT
(n + k) + k1 is V7() V8() V9() V13() V14() ext-real V58() Element of NAT
n2 . ((n + k) + k1) is Element of K32(X)
n + k1 is V7() V8() V9() V13() V14() ext-real V58() Element of NAT
k + (n + k1) is V7() V8() V9() V13() V14() ext-real V58() Element of NAT
k1 . (k + (n + k1)) is Element of K32(X)
k + k1 is V7() V8() V9() V13() V14() ext-real V58() Element of NAT
n + (k + k1) is V7() V8() V9() V13() V14() ext-real V58() Element of NAT
n2 . (n + (k + k1)) is Element of K32(X)
k1 . (n + (k + k1)) is Element of K32(X)
(n2 . (n + (k + k1))) \+\ (k1 . (n + (k + k1))) is Element of K10(X)
K8((n2 . (n + (k + k1))),(k1 . (n + (k + k1)))) is set
K8((k1 . (n + (k + k1))),(n2 . (n + (k + k1)))) is set
K6(K8((n2 . (n + (k + k1))),(k1 . (n + (k + k1)))),K8((k1 . (n + (k + k1))),(n2 . (n + (k + k1))))) is set
(X,n2,k1) . (n + (k + k1)) 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)))
lim_sup 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)))
lim_sup (X,A,A1) is Element of K10(X)
lim_sup A1 is Element of K10(X)
(lim_sup A) /\ (lim_sup A1) 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)))
lim_sup x is Element of K10(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)))
(X,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)))
lim_sup (X,x,n2) is Element of K10(X)
lim_sup n2 is Element of K10(X)
(lim_sup x) /\ (lim_sup n2) is Element of K10(X)
k1 is set
lim_inf x is Element of K10(X)
k is V7() V8() V9() V13() V14() ext-real V58() Element of NAT
n is V7() V8() V9() V13() V14() ext-real V58() Element of NAT
n + k is V7() V8() V9() V13() V14() ext-real V58() Element of NAT
k1 is V7() V8() V9() V13() V14() ext-real V58() Element of NAT
(n + k) + k1 is V7() V8() V9() V13() V14() ext-real V58() Element of NAT
n2 . ((n + k) + k1) is Element of K32(X)
n + k1 is V7() V8() V9() V13() V14() ext-real V58() Element of NAT
k + (n + k1) is V7() V8() V9() V13() V14() ext-real V58() Element of NAT
x . (k + (n + k1)) is Element of K32(X)
k + k1 is V7() V8() V9() V13() V14() ext-real V58() Element of NAT
n + (k + k1) is V7() V8() V9() V13() V14() ext-real V58() Element of NAT
x . (n + (k + k1)) is Element of K32(X)
n2 . (n + (k + k1)) is Element of K32(X)
(x . (n + (k + k1))) /\ (n2 . (n + (k + k1))) is Element of K10(X)
(X,x,n2) . (n + (k + k1)) 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)))
lim_sup 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)))
lim_sup (X,A1,A) is Element of K10(X)
lim_sup A1 is Element of K10(X)
(lim_sup A1) \ (lim_sup A) is Element of K10(X)
x is set
n2 is V7() V8() V9() V13() V14() ext-real V58() Element of NAT
k1 is V7() V8() V9() V13() V14() ext-real V58() Element of NAT
n2 + k1 is V7() V8() V9() V13() V14() ext-real V58() Element of NAT
(X,A1,A) . (n2 + k1) is Element of K32(X)
A1 . (n2 + k1) is Element of K32(X)
A . (n2 + k1) is Element of K32(X)
(A1 . (n2 + k1)) \ (A . (n2 + k1)) is Element of K10(X)
n2 is V7() V8() V9() V13() V14() ext-real V58() Element of NAT
k1 is V7() V8() V9() V13() V14() ext-real V58() Element of NAT
n2 + k1 is V7() V8() V9() V13() V14() ext-real V58() Element of NAT
A1 . (n2 + k1) is Element of K32(X)
A . (n2 + k1) is Element of K32(X)
lim_inf A is Element of K10(X)
n2 is V7() V8() V9() V13() V14() ext-real V58() Element of NAT
k1 is V7() V8() V9() V13() V14() ext-real V58() Element of NAT
n2 + k1 is V7() V8() V9() V13() V14() ext-real V58() Element of NAT
A1 . (n2 + k1) is Element of K32(X)
A . (n2 + k1) is Element of K32(X)
lim_inf 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)))
lim_sup 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)))
lim_sup (X,A,A1) is Element of K10(X)
lim_sup A1 is Element of K10(X)
(lim_sup A) \+\ (lim_sup A1) is Element of K10(X)
K8((lim_sup A),(lim_sup A1)) is set
K8((lim_sup A1),(lim_sup A)) is set
K6(K8((lim_sup A),(lim_sup A1)),K8((lim_sup A1),(lim_sup 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)))
(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)))
lim_sup (X,(X,A,A1),(X,A1,A)) is Element of K10(X)
lim_sup (X,A,A1) is Element of K10(X)
lim_sup (X,A1,A) is Element of K10(X)
(lim_sup (X,A,A1)) \/ (lim_sup (X,A1,A)) is Element of K10(X)
(lim_sup A) \ (lim_sup A1) is Element of K10(X)
((lim_sup A) \ (lim_sup A1)) \/ (lim_sup (X,A1,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)))
lim_inf (X,A1,A) is Element of K10(X)
lim_inf A1 is Element of K10(X)
A /\ (lim_inf A1) is Element of K10(X)
inferior_setsequence A1 is V1() V18() V21( NAT ) V22(K32(X)) Function-like V28( NAT ) V32( NAT ,K32(X)) Element of K10(K11(NAT,K32(X)))
inferior_setsequence (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)))
n2 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,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)))
k1 is V7() V8() V9() V13() V14() ext-real V58() Element of NAT
n2 . k1 is set
(X,x,A) . k1 is set
n2 . k1 is Element of K32(X)
x . k1 is Element of K32(X)
A /\ (x . k1) is Element of K10(X)
(X,x,A) . k1 is Element of K32(X)
Union n2 is Element of K10(X)
Union x is Element of K10(X)
A /\ (Union 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)))
lim_inf (X,A1,A) is Element of K10(X)
lim_inf A1 is Element of K10(X)
A \/ (lim_inf A1) is Element of K10(X)
inferior_setsequence A1 is V1() V18() V21( NAT ) V22(K32(X)) Function-like V28( NAT ) V32( NAT ,K32(X)) Element of K10(K11(NAT,K32(X)))
inferior_setsequence (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)))
n2 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,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)))
k1 is V7() V8() V9() V13() V14() ext-real V58() Element of NAT
n2 . k1 is set
(X,x,A) . k1 is set
n2 . k1 is Element of K32(X)
x . k1 is Element of K32(X)
A \/ (x . k1) is Element of K10(X)
(X,x,A) . k1 is Element of K32(X)
Union n2 is Element of K10(X)
Union x is Element of K10(X)
A \/ (Union 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)))
lim_inf (X,A1,A) is Element of K10(X)
lim_inf A1 is Element of K10(X)
A \ (lim_inf A1) is Element of K10(X)
x is set
n2 is V7() V8() V9() V13() V14() ext-real V58() Element of NAT
k1 is V7() V8() V9() V13() V14() ext-real V58() Element of NAT
n2 + k1 is V7() V8() V9() V13() V14() ext-real V58() Element of NAT
(X,A1,A) . (n2 + k1) is Element of K32(X)
A1 . (n2 + k1) is Element of K32(X)
A \ (A1 . (n2 + k1)) is Element of K10(X)
k1 is V7() V8() V9() V13() V14() ext-real V58() Element of NAT
k1 + n2 is V7() V8() V9() V13() V14() ext-real V58() Element of NAT
A1 . (k1 + 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)))
lim_inf (X,A1,A) is Element of K10(X)
lim_inf A1 is Element of K10(X)
(lim_inf A1) \ A is Element of K10(X)
inferior_setsequence A1 is V1() V18() V21( NAT ) V22(K32(X)) Function-like V28( NAT ) V32( NAT ,K32(X)) Element of K10(K11(NAT,K32(X)))
inferior_setsequence (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)))
n2 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,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)))
k1 is V7() V8() V9() V13() V14() ext-real V58() Element of NAT
n2 . k1 is set
(X,x,A) . k1 is set
n2 . k1 is Element of K32(X)
x . k1 is Element of K32(X)
(x . k1) \ A is Element of K10(X)
(X,x,A) . k1 is Element of K32(X)
Union n2 is Element of K10(X)
Union x is Element of K10(X)
(Union 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)))
lim_inf (X,A1,A) is Element of K10(X)
lim_inf A1 is Element of K10(X)
A \+\ (lim_inf A1) is Element of K10(X)
K8(A,(lim_inf A1)) is set
K8((lim_inf A1),A) is set
K6(K8(A,(lim_inf A1)),K8((lim_inf A1),A)) is set
x is set
n2 is V7() V8() V9() V13() V14() ext-real V58() Element of NAT
k1 is V7() V8() V9() V13() V14() ext-real V58() Element of NAT
n2 + k1 is V7() V8() V9() V13() V14() ext-real V58() Element of NAT
(X,A1,A) . (n2 + k1) is Element of K32(X)
A1 . (n2 + k1) is Element of K32(X)
A \+\ (A1 . (n2 + k1)) is Element of K10(X)
K8(A,(A1 . (n2 + k1))) is set
K8((A1 . (n2 + k1)),A) is set
K6(K8(A,(A1 . (n2 + k1))),K8((A1 . (n2 + k1)),A)) is set
k1 is V7() V8() V9() V13() V14() ext-real V58() Element of NAT
n2 + k1 is V7() V8() V9() V13() V14() ext-real V58() Element of NAT
A1 . (n2 + k1) is Element of K32(X)
k1 is V7() V8() V9() V13() V14() ext-real V58() Element of NAT
k1 is V7() V8() V9() V13() V14() ext-real V58() Element of NAT
k1 + n2 is V7() V8() V9() V13() V14() ext-real V58() Element of NAT
A1 . (k1 + n2) is Element of K32(X)
k is V7() V8() V9() V13() V14() ext-real V58() Element of NAT
k1 is V7() V8() V9() V13() V14() ext-real V58() Element of NAT
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)))
lim_inf (X,A1,A) is Element of K10(X)
lim_inf A1 is Element of K10(X)
A \ (lim_inf A1) is Element of K10(X)
x is set
lim_sup A1 is Element of K10(X)
A \ (lim_sup A1) is Element of K10(X)
n2 is V7() V8() V9() V13() V14() ext-real V58() Element of NAT
k1 is V7() V8() V9() V13() V14() ext-real V58() Element of NAT
k is V7() V8() V9() V13() V14() ext-real V58() Element of NAT
k1 + k is V7() V8() V9() V13() V14() ext-real V58() Element of NAT
(X,A1,A) . (k1 + k) is Element of K32(X)
A1 . (k1 + k) is Element of K32(X)
A \ (A1 . (k1 + k)) is Element of K10(X)
k1 is V7() V8() V9() V13() V14() ext-real V58() Element of NAT
n2 + k1 is V7() V8() V9() V13() V14() ext-real V58() Element of NAT
A1 . (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)))
lim_inf (X,A1,A) is Element of K10(X)
lim_inf A1 is Element of K10(X)
A \+\ (lim_inf A1) is Element of K10(X)
K8(A,(lim_inf A1)) is set
K8((lim_inf A1),A) is set
K6(K8(A,(lim_inf A1)),K8((lim_inf A1),A)) is set
x is set
lim_sup A1 is Element of K10(X)
n2 is V7() V8() V9() V13() V14() ext-real V58() Element of NAT
k1 is V7() V8() V9() V13() V14() ext-real V58() Element of NAT
n2 + k1 is V7() V8() V9() V13() V14() ext-real V58() Element of NAT
A1 . (n2 + k1) is Element of K32(X)
A \+\ (A1 . (n2 + k1)) is Element of K10(X)
K8(A,(A1 . (n2 + k1))) is set
K8((A1 . (n2 + k1)),A) is set
K6(K8(A,(A1 . (n2 + k1))),K8((A1 . (n2 + k1)),A)) is set
(X,A1,A) . (n2 + k1) is Element of K32(X)
n2 is V7() V8() V9() V13() V14() ext-real V58() Element of NAT
k1 is V7() V8() V9() V13() V14() ext-real V58() Element of NAT
n2 + k1 is V7() V8() V9() V13() V14() ext-real V58() Element of NAT
A1 . (n2 + k1) is Element of K32(X)
A \+\ (A1 . (n2 + k1)) is Element of K10(X)
K8(A,(A1 . (n2 + k1))) is set
K8((A1 . (n2 + k1)),A) is set
K6(K8(A,(A1 . (n2 + k1))),K8((A1 . (n2 + k1)),A)) is set
(X,A1,A) . (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)))
lim_sup (X,A1,A) is Element of K10(X)
lim_sup A1 is Element of K10(X)
A /\ (lim_sup A1) is Element of K10(X)
superior_setsequence A1 is V1() V18() V21( NAT ) V22(K32(X)) Function-like V28( NAT ) V32( NAT ,K32(X)) Element of K10(K11(NAT,K32(X)))
superior_setsequence (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)))
n2 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,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)))
k1 is V7() V8() V9() V13() V14() ext-real V58() Element of NAT
n2 . k1 is set
(X,x,A) . k1 is set
n2 . k1 is Element of K32(X)
x . k1 is Element of K32(X)
A /\ (x . k1) is Element of K10(X)
(X,x,A) . k1 is Element of K32(X)
Intersection n2 is Element of K10(X)
Intersection x is Element of K10(X)
A /\ (Intersection 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)))
lim_sup (X,A1,A) is Element of K10(X)
lim_sup A1 is Element of K10(X)
A \/ (lim_sup A1) is Element of K10(X)
superior_setsequence A1 is V1() V18() V21( NAT ) V22(K32(X)) Function-like V28( NAT ) V32( NAT ,K32(X)) Element of K10(K11(NAT,K32(X)))
superior_setsequence (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)))
n2 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,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)))
k1 is V7() V8() V9() V13() V14() ext-real V58() Element of NAT
n2 . k1 is set
(X,x,A) . k1 is set
n2 . k1 is Element of K32(X)
x . k1 is Element of K32(X)
A \/ (x . k1) is Element of K10(X)
(X,x,A) . k1 is Element of K32(X)
Intersection n2 is Element of K10(X)
Intersection x is Element of K10(X)
A \/ (Intersection 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)))
lim_sup A1 is Element of K10(X)
A \ (lim_sup 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)))
lim_sup (X,A1,A) is Element of K10(X)
x is set
n2 is V7() V8() V9() V13() V14() ext-real V58() Element of NAT
k1 is V7() V8() V9() V13() V14() ext-real V58() Element of NAT
k is V7() V8() V9() V13() V14() ext-real V58() Element of NAT
k1 + k is V7() V8() V9() V13() V14() ext-real V58() Element of NAT
(X,A1,A) . (k1 + k) is Element of K32(X)
A1 . (k1 + k) is Element of K32(X)
A \ (A1 . (k1 + k)) is Element of K10(X)
n2 + k1 is V7() V8() V9() V13() V14() ext-real V58() Element of NAT
A1 . (n2 + k1) is Element of K32(X)
k is V7() V8() V9() V13() V14() ext-real V58() Element of NAT
k1 + k is V7() V8() V9() V13() V14() ext-real V58() Element of NAT
A1 . (k1 + k) 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)))
lim_sup (X,A1,A) is Element of K10(X)
lim_sup A1 is Element of K10(X)
(lim_sup A1) \ A is Element of K10(X)
superior_setsequence A1 is V1() V18() V21( NAT ) V22(K32(X)) Function-like V28( NAT ) V32( NAT ,K32(X)) Element of K10(K11(NAT,K32(X)))
superior_setsequence (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)))
n2 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,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)))
k1 is V7() V8() V9() V13() V14() ext-real V58() Element of NAT
n2 . k1 is set
(X,x,A) . k1 is set
n2 . k1 is Element of K32(X)
x . k1 is Element of K32(X)
(x . k1) \ A is Element of K10(X)
(X,x,A) . k1 is Element of K32(X)
Intersection n2 is Element of K10(X)
Intersection x is Element of K10(X)
(Intersection 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)))
lim_sup A1 is Element of K10(X)
A \+\ (lim_sup A1) is Element of K10(X)
K8(A,(lim_sup A1)) is set
K8((lim_sup A1),A) is set
K6(K8(A,(lim_sup A1)),K8((lim_sup 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)))
lim_sup (X,A1,A) is Element of K10(X)
x is V7() V8() V9() V13() V14() ext-real V58() Element of NAT
(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 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)))
lim_sup (X,A1,A) is Element of K10(X)
lim_sup A1 is Element of K10(X)
A \ (lim_sup A1) is Element of K10(X)
x is set
n2 is V7() V8() V9() V13() V14() ext-real V58() Element of NAT
k1 is V7() V8() V9() V13() V14() ext-real V58() Element of NAT
n2 + k1 is V7() V8() V9() V13() V14() ext-real V58() Element of NAT
(X,A1,A) . (n2 + k1) is Element of K32(X)
A1 . (n2 + k1) is Element of K32(X)
A \ (A1 . (n2 + k1)) is Element of K10(X)
n2 is V7() V8() V9() V13() V14() ext-real V58() Element of NAT
k1 is V7() V8() V9() V13() V14() ext-real V58() Element of NAT
n2 + k1 is V7() V8() V9() V13() V14() ext-real V58() Element of NAT
A1 . (n2 + k1) is Element of K32(X)
n2 is V7() V8() V9() V13() V14() ext-real V58() Element of NAT
k1 is V7() V8() V9() V13() V14() ext-real V58() Element of NAT
n2 + k1 is V7() V8() V9() V13() V14() ext-real V58() Element of NAT
A1 . (n2 + k1) is Element of K32(X)
lim_inf A1 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)))
lim_sup (X,A1,A) is Element of K10(X)
lim_sup A1 is Element of K10(X)
A \+\ (lim_sup A1) is Element of K10(X)
K8(A,(lim_sup A1)) is set
K8((lim_sup A1),A) is set
K6(K8(A,(lim_sup A1)),K8((lim_sup A1),A)) is set
x is set
n2 is V7() V8() V9() V13() V14() ext-real V58() Element of NAT
k1 is V7() V8() V9() V13() V14() ext-real V58() Element of NAT
n2 + k1 is V7() V8() V9() V13() V14() ext-real V58() Element of NAT
(X,A1,A) . (n2 + k1) is Element of K32(X)
A1 . (n2 + k1) is Element of K32(X)
A \+\ (A1 . (n2 + k1)) is Element of K10(X)
K8(A,(A1 . (n2 + k1))) is set
K8((A1 . (n2 + k1)),A) is set
K6(K8(A,(A1 . (n2 + k1))),K8((A1 . (n2 + k1)),A)) is set
n2 is V7() V8() V9() V13() V14() ext-real V58() Element of NAT
k1 is V7() V8() V9() V13() V14() ext-real V58() Element of NAT
n2 + k1 is V7() V8() V9() V13() V14() ext-real V58() Element of NAT
A1 . (n2 + k1) is Element of K32(X)
k is V7() V8() V9() V13() V14() ext-real V58() Element of NAT
n2 + k is V7() V8() V9() V13() V14() ext-real V58() Element of NAT
A1 . (n2 + k) is Element of K32(X)
lim_inf A1 is Element of K10(X)
n2 is V7() V8() V9() V13() V14() ext-real V58() Element of NAT
k1 is V7() V8() V9() V13() V14() ext-real V58() Element of NAT
n2 + k1 is V7() V8() V9() V13() V14() ext-real V58() Element of NAT
A1 . (n2 + k1) is Element of K32(X)
k is V7() V8() V9() V13() V14() ext-real V58() Element of NAT
n2 + k is V7() V8() V9() V13() V14() ext-real V58() Element of NAT
A1 . (n2 + k) 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)))
lim_sup 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)))
lim_sup (X,A,A1) is Element of K10(X)
lim_sup A1 is Element of K10(X)
(lim_sup A) /\ (lim_sup A1) is Element of K10(X)
lim_inf (X,A,A1) is Element of K10(X)
lim_inf A is Element of K10(X)
lim_inf A1 is Element of K10(X)
(lim_inf A) /\ (lim_inf A1) is Element of K10(X)
(lim_sup A) /\ (lim_inf A1) 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)))
lim_sup 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)))
lim_sup (X,A,A1) is Element of K10(X)
lim_sup A1 is Element of K10(X)
(lim_sup A) \/ (lim_sup A1) is Element of K10(X)
lim_inf (X,A,A1) is Element of K10(X)
lim_inf A is Element of K10(X)
lim_inf A1 is Element of K10(X)
(lim_inf A) \/ (lim_inf A1) is Element of K10(X)
(lim_sup A) \/ (lim_inf A1) 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)))
lim_sup 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)))
lim_sup (X,A,A1) is Element of K10(X)
lim_sup A1 is Element of K10(X)
(lim_sup A) \ (lim_sup A1) is Element of K10(X)
lim_inf (X,A,A1) is Element of K10(X)
lim_inf A is Element of K10(X)
lim_inf A1 is Element of K10(X)
(lim_inf A) \ (lim_inf A1) is Element of K10(X)
(lim_sup A) \ (lim_inf A1) 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)))
lim_sup 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)))
lim_sup (X,A,A1) is Element of K10(X)
lim_sup A1 is Element of K10(X)
(lim_sup A) \+\ (lim_sup A1) is Element of K10(X)
K8((lim_sup A),(lim_sup A1)) is set
K8((lim_sup A1),(lim_sup A)) is set
K6(K8((lim_sup A),(lim_sup A1)),K8((lim_sup A1),(lim_sup A))) is set
lim_inf (X,A,A1) is Element of K10(X)
lim_inf A is Element of K10(X)
lim_inf A1 is Element of K10(X)
(lim_inf A) \+\ (lim_inf A1) is Element of K10(X)
K8((lim_inf A),(lim_inf A1)) is set
K8((lim_inf A1),(lim_inf A)) is set
K6(K8((lim_inf A),(lim_inf A1)),K8((lim_inf A1),(lim_inf A))) is set
(lim_sup A) \+\ (lim_inf A1) is Element of K10(X)
K8((lim_sup A),(lim_inf A1)) is set
K8((lim_inf A1),(lim_sup A)) is set
K6(K8((lim_sup A),(lim_inf A1)),K8((lim_inf A1),(lim_sup A))) is set
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)))
lim_sup (X,A1,A) is Element of K10(X)
lim_sup A1 is Element of K10(X)
A /\ (lim_sup A1) is Element of K10(X)
lim_inf (X,A1,A) is Element of K10(X)
lim_inf A1 is Element of K10(X)
A /\ (lim_inf A1) 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)))
lim_sup (X,A1,A) is Element of K10(X)
lim_sup A1 is Element of K10(X)
A \/ (lim_sup A1) is Element of K10(X)
lim_inf (X,A1,A) is Element of K10(X)
lim_inf A1 is Element of K10(X)
A \/ (lim_inf A1) 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)))
lim_sup (X,A1,A) is Element of K10(X)
lim_sup A1 is Element of K10(X)
A \ (lim_sup A1) is Element of K10(X)
lim_inf (X,A1,A) is Element of K10(X)
lim_inf A1 is Element of K10(X)
A \ (lim_inf A1) 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)))
lim_sup (X,A1,A) is Element of K10(X)
lim_sup A1 is Element of K10(X)
(lim_sup A1) \ A is Element of K10(X)
lim_inf (X,A1,A) is Element of K10(X)
lim_inf A1 is Element of K10(X)
(lim_inf A1) \ 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)))
lim_sup (X,A1,A) is Element of K10(X)
lim_sup A1 is Element of K10(X)
A \+\ (lim_sup A1) is Element of K10(X)
K8(A,(lim_sup A1)) is set
K8((lim_sup A1),A) is set
K6(K8(A,(lim_sup A1)),K8((lim_sup A1),A)) is set
lim_inf (X,A1,A) is Element of K10(X)
lim_inf A1 is Element of K10(X)
A \+\ (lim_inf A1) is Element of K10(X)
K8(A,(lim_inf A1)) is set
K8((lim_inf A1),A) is set
K6(K8(A,(lim_inf A1)),K8((lim_inf A1),A)) is set