REAL is complex-membered ext-real-membered real-membered V7() set
NAT is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V7() non empty non trivial epsilon-transitive epsilon-connected ordinal limit_ordinal non finite cardinal limit_cardinal ordinal-membered Element of bool REAL
bool REAL is non empty set
NAT is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V7() non empty non trivial epsilon-transitive epsilon-connected ordinal limit_ordinal non finite cardinal limit_cardinal ordinal-membered set
bool NAT is non empty non trivial non finite set
bool NAT is non empty non trivial non finite set
0 is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V7() V8() empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional ext-real non positive non negative complex-valued ext-real-valued real-valued natural-valued finite finite-yielding V53() cardinal {} -element Ordinal-yielding increasing V67() real V70() V71() decreasing non-decreasing non-increasing V79() ordinal-membered Element of NAT
RAT is complex-membered ext-real-membered real-membered rational-membered V7() set
{} is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V7() empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional ext-real non positive non negative complex-valued ext-real-valued real-valued natural-valued finite finite-yielding V53() cardinal {} -element Ordinal-yielding increasing V67() V71() decreasing non-decreasing non-increasing V79() ordinal-membered set
the complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V7() empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional ext-real non positive non negative complex-valued ext-real-valued real-valued natural-valued finite finite-yielding V53() cardinal {} -element Ordinal-yielding increasing V67() V71() decreasing non-decreasing non-increasing V79() ordinal-membered set is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V7() empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional ext-real non positive non negative complex-valued ext-real-valued real-valued natural-valued finite finite-yielding V53() cardinal {} -element Ordinal-yielding increasing V67() V71() decreasing non-decreasing non-increasing V79() ordinal-membered set
1 is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V8() non empty epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative finite cardinal real V70() ordinal-membered Element of NAT
K158(NAT,0,1) is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered non empty finite V53() Element of bool NAT
K158(NAT,0,1) ^omega is non empty functional set
bool (K158(NAT,0,1) ^omega) is non empty set
[:NAT,REAL:] is Relation-like complex-valued ext-real-valued real-valued set
bool [:NAT,REAL:] is non empty set
K326() is set
{{},1} is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered non empty finite V53() set
INT is complex-membered ext-real-membered real-membered rational-membered integer-membered V7() set
K412() is set
bool K412() is non empty set
K413() is Element of bool K412()
K453() is non empty V136() L10()
the carrier of K453() is non empty set
K416( the carrier of K453()) is non empty M30( the carrier of K453())
K452(K453()) is Element of bool K416( the carrier of K453())
bool K416( the carrier of K453()) is non empty set
[:K452(K453()),NAT:] is Relation-like RAT -valued INT -valued complex-valued ext-real-valued real-valued natural-valued set
bool [:K452(K453()),NAT:] is non empty set
[:NAT,K452(K453()):] is Relation-like set
bool [:NAT,K452(K453()):] is non empty set
2 is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V8() non empty epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative finite cardinal real V70() ordinal-membered Element of NAT
K317(2,K326()) is M14(K326())
[:K317(2,K326()),K326():] is Relation-like set
bool [:K317(2,K326()),K326():] is non empty set
3 is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V8() non empty epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative finite cardinal real V70() ordinal-membered Element of NAT
K317(3,K326()) is M14(K326())
[:K317(3,K326()),K326():] is Relation-like set
bool [:K317(3,K326()),K326():] is non empty set
K509() is Relation-like K317(2,K326()) -defined K326() -valued Function-like quasi_total Element of bool [:K317(2,K326()),K326():]
{{}} is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered non empty trivial functional finite V53() 1 -element V90() set
O is epsilon-transitive epsilon-connected ordinal ordinal-membered set
A is epsilon-transitive epsilon-connected ordinal ordinal-membered set
O +^ A is epsilon-transitive epsilon-connected ordinal ordinal-membered set
(O +^ A) \ O is ordinal-membered Element of bool (O +^ A)
bool (O +^ A) is non empty set
C is set
B is epsilon-transitive epsilon-connected ordinal ordinal-membered set
B -^ O is epsilon-transitive epsilon-connected ordinal ordinal-membered set
c5 is epsilon-transitive epsilon-connected ordinal ordinal-membered set
O +^ c5 is epsilon-transitive epsilon-connected ordinal ordinal-membered set
B is epsilon-transitive epsilon-connected ordinal ordinal-membered set
O +^ B is epsilon-transitive epsilon-connected ordinal ordinal-membered set
O is epsilon-transitive epsilon-connected ordinal ordinal-membered set
A is epsilon-transitive epsilon-connected ordinal ordinal-membered set
C is epsilon-transitive epsilon-connected ordinal ordinal-membered set
B is epsilon-transitive epsilon-connected ordinal ordinal-membered set
O is set
A is set
{O} is non empty trivial finite 1 -element set
A \/ {O} is non empty set
(A \/ {O}) \ A is Element of bool (A \/ {O})
bool (A \/ {O}) is non empty set
O is set
succ O is non empty set
{O} is non empty trivial finite 1 -element set
O \/ {O} is non empty set
(succ O) \ O is Element of bool (succ O)
bool (succ O) is non empty set
O is Relation-like Function-like set
proj1 O is set
A is Relation-like set
O .: A is set
C is set
B is set
O . B is set
c5 is set
f is set
[c5,f] is V30() set
{c5,f} is non empty finite set
{c5} is non empty trivial finite 1 -element set
{{c5,f},{c5}} is non empty finite V53() set
O . (c5,f) is set
O . [c5,f] is set
B is set
c5 is set
[B,c5] is V30() set
{B,c5} is non empty finite set
{B} is non empty trivial finite 1 -element set
{{B,c5},{B}} is non empty finite V53() set
O . (B,c5) is set
O . [B,c5] is set
O is epsilon-transitive epsilon-connected ordinal ordinal-membered set
union O is epsilon-transitive epsilon-connected ordinal ordinal-membered set
A is epsilon-transitive epsilon-connected ordinal ordinal-membered set
O \ A is ordinal-membered Element of bool O
bool O is non empty set
inf (O \ A) is epsilon-transitive epsilon-connected ordinal ordinal-membered set
On (O \ A) is ordinal-membered set
K181((On (O \ A))) is set
sup (O \ A) is epsilon-transitive epsilon-connected ordinal ordinal-membered set
union (O \ A) is epsilon-transitive epsilon-connected ordinal ordinal-membered set
the epsilon-transitive epsilon-connected ordinal ordinal-membered Element of O \ A is epsilon-transitive epsilon-connected ordinal ordinal-membered Element of O \ A
B is epsilon-transitive epsilon-connected ordinal ordinal-membered set
B is set
c5 is set
f is epsilon-transitive epsilon-connected ordinal ordinal-membered set
f is epsilon-transitive epsilon-connected ordinal ordinal-membered set
f is epsilon-transitive epsilon-connected ordinal ordinal-membered set
O is epsilon-transitive epsilon-connected ordinal ordinal-membered set
A is epsilon-transitive epsilon-connected ordinal ordinal-membered set
O \ A is ordinal-membered Element of bool O
bool O is non empty set
the epsilon-transitive epsilon-connected ordinal ordinal-membered Element of O \ A is epsilon-transitive epsilon-connected ordinal ordinal-membered Element of O \ A
B is epsilon-transitive epsilon-connected ordinal ordinal-membered set
A +^ B is epsilon-transitive epsilon-connected ordinal ordinal-membered set
c5 is T-Sequence-like Relation-like Function-like set
proj1 c5 is epsilon-transitive epsilon-connected ordinal ordinal-membered set
f is set
c5 . f is set
k is set
c5 . k is set
f is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V8() epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal real V70() ordinal-membered Element of NAT
c5 . f is set
A +^ f is epsilon-transitive epsilon-connected ordinal ordinal-membered set
c9 is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V8() epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal real V70() ordinal-membered Element of NAT
c5 . c9 is set
A +^ c9 is epsilon-transitive epsilon-connected ordinal ordinal-membered set
proj2 c5 is set
A +^ NAT is epsilon-transitive epsilon-connected ordinal ordinal-membered set
f is set
k is set
c5 . k is set
f is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V8() epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal real V70() ordinal-membered Element of NAT
A +^ f is epsilon-transitive epsilon-connected ordinal ordinal-membered set
O is Relation-like Function-like set
proj1 O is set
A is Relation-like Function-like set
proj1 A is set
C is epsilon-transitive epsilon-connected ordinal ordinal-membered set
B is epsilon-transitive epsilon-connected ordinal ordinal-membered set
C \ B is ordinal-membered Element of bool C
bool C is non empty set
O is Relation-like Function-like set
proj1 O is set
A is epsilon-transitive epsilon-connected ordinal ordinal-membered set
C is epsilon-transitive epsilon-connected ordinal ordinal-membered set
A \ C is ordinal-membered Element of bool A
bool A is non empty set
B is epsilon-transitive epsilon-connected ordinal ordinal-membered set
c5 is epsilon-transitive epsilon-connected ordinal ordinal-membered set
f is epsilon-transitive epsilon-connected ordinal ordinal-membered set
O is Relation-like Function-like set
A is T-Sequence-like Relation-like Function-like set
proj1 A is epsilon-transitive epsilon-connected ordinal ordinal-membered set
proj1 O is set
(proj1 A) \ {} is ordinal-membered Element of bool (proj1 A)
bool (proj1 A) is non empty set
O is Relation-like Function-like set
A is Relation-like Function-like FinSequence-like set
len A is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V8() epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal real V70() ordinal-membered Element of NAT
succ (len A) is non empty epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative finite cardinal ordinal-membered set
{(len A)} is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered non empty trivial finite V53() 1 -element set
(len A) \/ {(len A)} is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered non empty finite set
proj1 O is set
C is non empty epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative finite cardinal ordinal-membered set
B is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V8() non empty epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative finite cardinal real V70() ordinal-membered Element of NAT
C \ B is finite ordinal-membered Element of bool C
bool C is non empty finite V53() set
f is set
dom A is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of bool NAT
k is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal ordinal-membered set
c5 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal ordinal-membered set
succ {} is non empty epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative finite cardinal ordinal-membered set
{} \/ {{}} is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered non empty finite V53() set
k is set
f is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V8() epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal real V70() ordinal-membered Element of NAT
f is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal ordinal-membered set
c5 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal ordinal-membered set
O is epsilon-transitive epsilon-connected ordinal ordinal-membered set
A is Relation-like Function-like set
proj1 A is set
C is epsilon-transitive epsilon-connected ordinal ordinal-membered set
B is epsilon-transitive epsilon-connected ordinal ordinal-membered set
C \ B is ordinal-membered Element of bool C
bool C is non empty set
the epsilon-transitive epsilon-connected ordinal ordinal-membered Element of C \ B is epsilon-transitive epsilon-connected ordinal ordinal-membered Element of C \ B
O \ O is ordinal-membered Element of bool O
bool O is non empty set
C is epsilon-transitive epsilon-connected ordinal ordinal-membered set
C \ O is ordinal-membered Element of bool C
bool C is non empty set
B is epsilon-transitive epsilon-connected ordinal ordinal-membered set
O is epsilon-transitive epsilon-connected ordinal ordinal-membered set
A is Relation-like Function-like set
proj1 A is set
sup (proj1 A) is epsilon-transitive epsilon-connected ordinal ordinal-membered set
C is epsilon-transitive epsilon-connected ordinal ordinal-membered set
B is epsilon-transitive epsilon-connected ordinal ordinal-membered set
C \ B is ordinal-membered Element of bool C
bool C is non empty set
the epsilon-transitive epsilon-connected ordinal ordinal-membered Element of C \ B is epsilon-transitive epsilon-connected ordinal ordinal-membered Element of C \ B
f is epsilon-transitive epsilon-connected ordinal ordinal-membered set
O \ f is ordinal-membered Element of bool O
bool O is non empty set
C is epsilon-transitive epsilon-connected ordinal ordinal-membered set
O \ C is ordinal-membered Element of bool O
bool O is non empty set
sup (proj1 A) is epsilon-transitive epsilon-connected ordinal ordinal-membered set
O is Relation-like Function-like set
C is epsilon-transitive epsilon-connected ordinal ordinal-membered set
proj1 O is set
A is T-Sequence-like Relation-like Function-like () set
proj1 A is epsilon-transitive epsilon-connected ordinal ordinal-membered set
O is Relation-like Function-like set
C is epsilon-transitive epsilon-connected ordinal ordinal-membered set
proj1 O is set
A is Relation-like Function-like FinSequence-like () set
dom A is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered Element of bool NAT
B is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal ordinal-membered set
len A is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V8() epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal real V70() ordinal-membered Element of NAT
O is Relation-like Function-like set
proj1 O is set
inf (proj1 O) is epsilon-transitive epsilon-connected ordinal ordinal-membered set
On (proj1 O) is ordinal-membered set
K181((On (proj1 O))) is set
C is epsilon-transitive epsilon-connected ordinal ordinal-membered set
O is Relation-like Function-like set
proj1 O is set
sup (proj1 O) is epsilon-transitive epsilon-connected ordinal ordinal-membered set
O is epsilon-transitive epsilon-connected ordinal ordinal-membered set
A is epsilon-transitive epsilon-connected ordinal ordinal-membered set
C is Relation-like Function-like set
proj1 C is set
sup (proj1 C) is epsilon-transitive epsilon-connected ordinal ordinal-membered set
O is Relation-like Function-like set
proj1 O is set
inf (proj1 O) is epsilon-transitive epsilon-connected ordinal ordinal-membered set
On (proj1 O) is ordinal-membered set
K181((On (proj1 O))) is set
C is epsilon-transitive epsilon-connected ordinal ordinal-membered set
B is epsilon-transitive epsilon-connected ordinal ordinal-membered set
A is epsilon-transitive epsilon-connected ordinal ordinal-membered set
C is epsilon-transitive epsilon-connected ordinal ordinal-membered set
B is epsilon-transitive epsilon-connected ordinal ordinal-membered set
sup (proj1 O) is epsilon-transitive epsilon-connected ordinal ordinal-membered set
C is epsilon-transitive epsilon-connected ordinal ordinal-membered set
B is epsilon-transitive epsilon-connected ordinal ordinal-membered set
A is epsilon-transitive epsilon-connected ordinal ordinal-membered set
C is epsilon-transitive epsilon-connected ordinal ordinal-membered set
B is epsilon-transitive epsilon-connected ordinal ordinal-membered set
sup (proj1 O) is epsilon-transitive epsilon-connected ordinal ordinal-membered set
O is Relation-like Function-like set
(O) is epsilon-transitive epsilon-connected ordinal ordinal-membered set
(O) is epsilon-transitive epsilon-connected ordinal ordinal-membered set
(O) -^ (O) is epsilon-transitive epsilon-connected ordinal ordinal-membered set
({}) is epsilon-transitive epsilon-connected ordinal ordinal-membered set
({}) is epsilon-transitive epsilon-connected ordinal ordinal-membered set
({}) is epsilon-transitive epsilon-connected ordinal ordinal-membered set
({}) -^ ({}) is epsilon-transitive epsilon-connected ordinal ordinal-membered set
dom {} is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V7() empty proper epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional ext-real non positive non negative complex-valued ext-real-valued real-valued natural-valued finite finite-yielding V53() cardinal {} -element Ordinal-yielding increasing V67() V71() decreasing non-decreasing non-increasing V79() ordinal-membered () ( {} ) Element of bool NAT
O is epsilon-transitive epsilon-connected ordinal ordinal-membered set
O is Relation-like Function-like set
(O) is epsilon-transitive epsilon-connected ordinal ordinal-membered set
proj1 O is set
sup (proj1 O) is epsilon-transitive epsilon-connected ordinal ordinal-membered set
On (proj1 O) is ordinal-membered set
A is set
A is epsilon-transitive epsilon-connected ordinal ordinal-membered set
A is epsilon-transitive epsilon-connected ordinal ordinal-membered set
O is Relation-like Function-like set
(O) is epsilon-transitive epsilon-connected ordinal ordinal-membered set
proj1 O is set
sup (proj1 O) is epsilon-transitive epsilon-connected ordinal ordinal-membered set
O is epsilon-transitive epsilon-connected ordinal ordinal-membered set
A is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V7() empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional ext-real non positive non negative complex-valued ext-real-valued real-valued natural-valued finite finite-yielding V53() cardinal {} -element Ordinal-yielding increasing V67() V71() decreasing non-decreasing non-increasing V79() ordinal-membered () ( {} ) set
C is epsilon-transitive epsilon-connected ordinal ordinal-membered set
proj1 A is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V7() empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional ext-real non positive non negative complex-valued ext-real-valued real-valued natural-valued finite finite-yielding V53() cardinal {} -element Ordinal-yielding increasing V67() V71() decreasing non-decreasing non-increasing V79() ordinal-membered () ( {} ) set
C is set
A is set
O is epsilon-transitive epsilon-connected ordinal ordinal-membered set
[:C,A:] is Relation-like set
bool [:C,A:] is non empty set
{} [:C,A:] is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V7() empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional ext-real non positive non negative complex-valued ext-real-valued real-valued natural-valued finite finite-yielding V53() cardinal {} -element Ordinal-yielding increasing V67() V71() decreasing non-decreasing non-increasing V79() ordinal-membered () ( {} ) Element of bool [:C,A:]
B is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V7() empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional ext-real non positive non negative complex-valued ext-real-valued real-valued natural-valued finite finite-yielding V53() cardinal {} -element Ordinal-yielding increasing V67() V71() decreasing non-decreasing non-increasing V79() ordinal-membered () ( {} ) Element of bool [:C,A:]
O is Relation-like Function-like () set
proj1 O is set
A is epsilon-transitive epsilon-connected ordinal ordinal-membered set
C is epsilon-transitive epsilon-connected ordinal ordinal-membered set
A \ C is ordinal-membered Element of bool A
bool A is non empty set
O is Relation-like Function-like () set
proj1 O is ordinal-membered set
sup (proj1 O) is epsilon-transitive epsilon-connected ordinal ordinal-membered set
proj1 O is ordinal-membered set
sup (proj1 O) is epsilon-transitive epsilon-connected ordinal ordinal-membered set
O is Relation-like Function-like () set
proj1 O is ordinal-membered set
A is epsilon-transitive epsilon-connected ordinal ordinal-membered set
C is epsilon-transitive epsilon-connected ordinal ordinal-membered set
A \ C is ordinal-membered Element of bool A
bool A is non empty set
the epsilon-transitive epsilon-connected ordinal ordinal-membered Element of A \ C is epsilon-transitive epsilon-connected ordinal ordinal-membered Element of A \ C
O is Relation-like Function-like set
(O) is epsilon-transitive epsilon-connected ordinal ordinal-membered set
proj1 O is set
inf (proj1 O) is epsilon-transitive epsilon-connected ordinal ordinal-membered set
On (proj1 O) is ordinal-membered set
K181((On (proj1 O))) is set
B is epsilon-transitive epsilon-connected ordinal ordinal-membered set
the epsilon-transitive epsilon-connected ordinal ordinal-membered Element of On (proj1 O) is epsilon-transitive epsilon-connected ordinal ordinal-membered Element of On (proj1 O)
B is epsilon-transitive epsilon-connected ordinal ordinal-membered set
O is Relation-like Function-like set
(O) is epsilon-transitive epsilon-connected ordinal ordinal-membered set
proj1 O is set
inf (proj1 O) is epsilon-transitive epsilon-connected ordinal ordinal-membered set
On (proj1 O) is ordinal-membered set
K181((On (proj1 O))) is set
O is Relation-like Function-like () set
proj1 O is ordinal-membered set
(O) is epsilon-transitive epsilon-connected ordinal ordinal-membered set
(O) is epsilon-transitive epsilon-connected ordinal ordinal-membered set
(O) \ (O) is ordinal-membered Element of bool (O)
bool (O) is non empty set
A is epsilon-transitive epsilon-connected ordinal ordinal-membered set
C is epsilon-transitive epsilon-connected ordinal ordinal-membered set
A \ C is ordinal-membered Element of bool A
bool A is non empty set
sup (proj1 O) is epsilon-transitive epsilon-connected ordinal ordinal-membered set
inf (proj1 O) is epsilon-transitive epsilon-connected ordinal ordinal-membered set
On (proj1 O) is ordinal-membered set
K181((On (proj1 O))) is set
B is set
B is set
c5 is epsilon-transitive epsilon-connected ordinal ordinal-membered set
f is epsilon-transitive epsilon-connected ordinal ordinal-membered set
O is epsilon-transitive epsilon-connected ordinal ordinal-membered set
A is epsilon-transitive epsilon-connected ordinal ordinal-membered set
O \ A is ordinal-membered Element of bool O
bool O is non empty set
C is Relation-like Function-like () set
proj1 C is ordinal-membered set
(C) is epsilon-transitive epsilon-connected ordinal ordinal-membered set
(C) is epsilon-transitive epsilon-connected ordinal ordinal-membered set
the epsilon-transitive epsilon-connected ordinal ordinal-membered Element of proj1 C is epsilon-transitive epsilon-connected ordinal ordinal-membered Element of proj1 C
sup (proj1 C) is epsilon-transitive epsilon-connected ordinal ordinal-membered set
c5 is epsilon-transitive epsilon-connected ordinal ordinal-membered set
c5 is epsilon-transitive epsilon-connected ordinal ordinal-membered set
sup O is epsilon-transitive epsilon-connected ordinal ordinal-membered set
O is T-Sequence-like Relation-like Function-like () ( {} ) set
(O) is epsilon-transitive epsilon-connected ordinal ordinal-membered set
(O) is epsilon-transitive epsilon-connected ordinal ordinal-membered set
proj1 O is epsilon-transitive epsilon-connected ordinal ordinal-membered set
(O) is epsilon-transitive epsilon-connected ordinal ordinal-membered set
(O) -^ (O) is epsilon-transitive epsilon-connected ordinal ordinal-membered set
(proj1 O) \ {} is ordinal-membered Element of bool (proj1 O)
bool (proj1 O) is non empty set
O is epsilon-transitive epsilon-connected ordinal ordinal-membered set
C is set
A is epsilon-transitive epsilon-connected ordinal ordinal-membered set
the complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V7() empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural Relation-like non-empty empty-yielding O -defined C -valued Function-like one-to-one constant functional ext-real non positive non negative complex-valued ext-real-valued real-valued natural-valued finite finite-yielding V53() cardinal {} -element Ordinal-yielding increasing V67() V71() decreasing non-decreasing non-increasing V79() ordinal-membered () ( {} ) set is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V7() empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural Relation-like non-empty empty-yielding O -defined C -valued Function-like one-to-one constant functional ext-real non positive non negative complex-valued ext-real-valued real-valued natural-valued finite finite-yielding V53() cardinal {} -element Ordinal-yielding increasing V67() V71() decreasing non-decreasing non-increasing V79() ordinal-membered () ( {} ) set
O is epsilon-transitive epsilon-connected ordinal ordinal-membered set
A is set
[O,A] is V30() set
{O,A} is non empty finite set
{O} is non empty trivial finite 1 -element set
{{O,A},{O}} is non empty finite V53() set
{[O,A]} is non empty trivial Relation-like Function-like constant finite 1 -element set
succ O is non empty epsilon-transitive epsilon-connected ordinal ordinal-membered set
O \/ {O} is non empty set
proj1 {[O,A]} is non empty trivial finite 1 -element set
(succ O) \ O is ordinal-membered Element of bool (succ O)
bool (succ O) is non empty set
O is epsilon-transitive epsilon-connected ordinal ordinal-membered set
A is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal ordinal-membered set
[O,A] is V30() set
{O,A} is non empty finite set
{O} is non empty trivial finite 1 -element set
{{O,A},{O}} is non empty finite V53() set
{[O,A]} is non empty trivial Relation-like Function-like constant finite 1 -element () set
C is Relation-like Function-like () set
proj2 C is set
{A} is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered non empty trivial finite V53() 1 -element set
O is epsilon-transitive epsilon-connected ordinal ordinal-membered set
A is real set
[O,A] is V30() set
{O,A} is non empty finite set
{O} is non empty trivial finite 1 -element set
{{O,A},{O}} is non empty finite V53() set
{[O,A]} is non empty trivial Relation-like Function-like constant finite 1 -element () set
C is Relation-like Function-like () set
proj2 C is set
{A} is complex-membered ext-real-membered real-membered non empty trivial finite 1 -element set
A is non empty set
O is epsilon-transitive epsilon-connected ordinal ordinal-membered set
C is Element of A
[O,C] is V30() set
{O,C} is non empty finite set
{O} is non empty trivial finite 1 -element set
{{O,C},{O}} is non empty finite V53() set
{[O,C]} is non empty trivial Relation-like Function-like constant finite 1 -element () set
B is Relation-like Function-like () set
proj2 B is set
{C} is non empty trivial finite 1 -element set
O is epsilon-transitive epsilon-connected ordinal ordinal-membered set
A is set
[O,A] is V30() set
{O,A} is non empty finite set
{O} is non empty trivial finite 1 -element set
{{O,A},{O}} is non empty finite V53() set
{[O,A]} is non empty trivial Relation-like Function-like constant finite 1 -element () set
succ O is non empty epsilon-transitive epsilon-connected ordinal ordinal-membered set
O \/ {O} is non empty set
C is Relation-like Function-like () set
proj1 C is ordinal-membered set
B is epsilon-transitive epsilon-connected ordinal ordinal-membered set
sup (proj1 C) is epsilon-transitive epsilon-connected ordinal ordinal-membered set
O is epsilon-transitive epsilon-connected ordinal ordinal-membered set
the epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal ordinal-membered set is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal ordinal-membered set
[O, the epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal ordinal-membered set ] is V30() set
{O, the epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal ordinal-membered set } is non empty finite set
{O} is non empty trivial finite 1 -element set
{{O, the epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal ordinal-membered set },{O}} is non empty finite V53() set
{[O, the epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal ordinal-membered set ]} is non empty trivial Relation-like RAT -valued Function-like constant complex-valued ext-real-valued real-valued natural-valued increasing decreasing non-decreasing non-increasing finite 1 -element () (O) ( succ O) set
succ O is non empty epsilon-transitive epsilon-connected ordinal ordinal-membered set
O \/ {O} is non empty set
C is Relation-like RAT -valued Function-like complex-valued ext-real-valued real-valued natural-valued () set
A is non empty set
the Element of A is Element of A
[O, the Element of A] is V30() set
{O, the Element of A} is non empty finite set
{O} is non empty trivial finite 1 -element set
{{O, the Element of A},{O}} is non empty finite V53() set
{[O, the Element of A]} is non empty trivial Relation-like A -valued Function-like constant finite 1 -element () (O) ( succ O) set
succ O is non empty epsilon-transitive epsilon-connected ordinal ordinal-membered set
O \/ {O} is non empty set
B is Relation-like A -valued Function-like () set
O is Relation-like Function-like () set
proj1 O is ordinal-membered set
union (proj1 O) is epsilon-transitive epsilon-connected ordinal ordinal-membered set
O . (union (proj1 O)) is set
O is T-Sequence-like Relation-like Function-like () ( {} ) set
last O is set
proj1 O is epsilon-transitive epsilon-connected ordinal ordinal-membered set
union (proj1 O) is epsilon-transitive epsilon-connected ordinal ordinal-membered set
O . (union (proj1 O)) is set
(O) is set
O is Relation-like Function-like finite () set
proj1 O is finite ordinal-membered set
A is epsilon-transitive epsilon-connected ordinal ordinal-membered set
O . A is set
C is epsilon-transitive epsilon-connected ordinal ordinal-membered set
O . C is set
B is epsilon-transitive epsilon-connected ordinal ordinal-membered set
c5 is epsilon-transitive epsilon-connected ordinal ordinal-membered set
B \ c5 is ordinal-membered Element of bool B
bool B is non empty set
f is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal ordinal-membered set
c5 +^ f is epsilon-transitive epsilon-connected ordinal ordinal-membered set
k is epsilon-transitive epsilon-connected ordinal ordinal-membered set
c5 +^ k is epsilon-transitive epsilon-connected ordinal ordinal-membered set
f is epsilon-transitive epsilon-connected ordinal ordinal-membered set
c5 +^ f is epsilon-transitive epsilon-connected ordinal ordinal-membered set
c9 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal ordinal-membered set
succ c9 is non empty epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative finite cardinal ordinal-membered set
{c9} is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered non empty trivial finite V53() 1 -element set
c9 \/ {c9} is non empty finite set
succ A is non empty epsilon-transitive epsilon-connected ordinal ordinal-membered set
{A} is non empty trivial finite 1 -element set
A \/ {A} is non empty set
c5 +^ (succ c9) is epsilon-transitive epsilon-connected ordinal ordinal-membered set
p is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal ordinal-membered set
q is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V8() epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal real V70() ordinal-membered Element of NAT
y is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal ordinal-membered set
q + y is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V8() epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal real V70() ordinal-membered Element of NAT
(succ A) +^ {} is epsilon-transitive epsilon-connected ordinal ordinal-membered set
O . H1( {} ) is set
b is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal ordinal-membered set
(succ A) +^ b is epsilon-transitive epsilon-connected ordinal ordinal-membered set
O . H1(b) is set
b + 1 is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V8() non empty epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative finite cardinal real V70() ordinal-membered Element of NAT
(succ A) +^ (b + 1) is epsilon-transitive epsilon-connected ordinal ordinal-membered set
O . H1(b + 1) is set
succ b is non empty epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative finite cardinal ordinal-membered set
{b} is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered non empty trivial finite V53() 1 -element set
b \/ {b} is non empty finite set
succ H1(b) is non empty epsilon-transitive epsilon-connected ordinal ordinal-membered set
{((succ A) +^ b)} is non empty trivial finite 1 -element set
((succ A) +^ b) \/ {((succ A) +^ b)} is non empty set
y is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V8() epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal real V70() ordinal-membered Element of NAT
q +^ y is epsilon-transitive epsilon-connected ordinal ordinal-membered set
c5 +^ (q +^ y) is epsilon-transitive epsilon-connected ordinal ordinal-membered set
(succ A) +^ y is epsilon-transitive epsilon-connected ordinal ordinal-membered set
O is Relation-like Function-like () set
(O) is epsilon-transitive epsilon-connected ordinal ordinal-membered set
(O) is epsilon-transitive epsilon-connected ordinal ordinal-membered set
(O) is epsilon-transitive epsilon-connected ordinal ordinal-membered set
(O) -^ (O) is epsilon-transitive epsilon-connected ordinal ordinal-membered set
proj1 O is ordinal-membered set
A is epsilon-transitive epsilon-connected ordinal ordinal-membered set
O . A is set
C is epsilon-transitive epsilon-connected ordinal ordinal-membered set
O . C is set
B is epsilon-transitive epsilon-connected ordinal ordinal-membered set
c5 is epsilon-transitive epsilon-connected ordinal ordinal-membered set
B \ c5 is ordinal-membered Element of bool B
bool B is non empty set
c5 +^ NAT is epsilon-transitive epsilon-connected ordinal ordinal-membered set
f is epsilon-transitive epsilon-connected ordinal ordinal-membered set
c5 +^ f is epsilon-transitive epsilon-connected ordinal ordinal-membered set
k is epsilon-transitive epsilon-connected ordinal ordinal-membered set
c5 +^ k is epsilon-transitive epsilon-connected ordinal ordinal-membered set
f is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal ordinal-membered set
succ f is non empty epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative finite cardinal ordinal-membered set
{f} is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered non empty trivial finite V53() 1 -element set
f \/ {f} is non empty finite set
succ A is non empty epsilon-transitive epsilon-connected ordinal ordinal-membered set
{A} is non empty trivial finite 1 -element set
A \/ {A} is non empty set
c5 +^ (succ f) is epsilon-transitive epsilon-connected ordinal ordinal-membered set
c9 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal ordinal-membered set
p is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V8() epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal real V70() ordinal-membered Element of NAT
q is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal ordinal-membered set
p + q is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V8() epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal real V70() ordinal-membered Element of NAT
(succ A) +^ {} is epsilon-transitive epsilon-connected ordinal ordinal-membered set
O . H1( {} ) is set
y is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal ordinal-membered set
(succ A) +^ y is epsilon-transitive epsilon-connected ordinal ordinal-membered set
O . H1(y) is set
y + 1 is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V8() non empty epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative finite cardinal real V70() ordinal-membered Element of NAT
(succ A) +^ (y + 1) is epsilon-transitive epsilon-connected ordinal ordinal-membered set
O . H1(y + 1) is set
succ y is non empty epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative finite cardinal ordinal-membered set
{y} is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered non empty trivial finite V53() 1 -element set
y \/ {y} is non empty finite set
succ H1(y) is non empty epsilon-transitive epsilon-connected ordinal ordinal-membered set
{((succ A) +^ y)} is non empty trivial finite 1 -element set
((succ A) +^ y) \/ {((succ A) +^ y)} is non empty set
y is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V8() epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal real V70() ordinal-membered Element of NAT
p +^ y is epsilon-transitive epsilon-connected ordinal ordinal-membered set
c5 +^ (p +^ y) is epsilon-transitive epsilon-connected ordinal ordinal-membered set
(succ A) +^ y is epsilon-transitive epsilon-connected ordinal ordinal-membered set
O is T-Sequence-like Relation-like Function-like () ( {} ) set
O . {} is set
proj1 O is epsilon-transitive epsilon-connected ordinal ordinal-membered set
A is T-Sequence-like Relation-like Function-like () ( {} ) set
proj1 A is epsilon-transitive epsilon-connected ordinal ordinal-membered set
C is epsilon-transitive epsilon-connected ordinal ordinal-membered set
O . C is set
succ C is non empty epsilon-transitive epsilon-connected ordinal ordinal-membered set
{C} is non empty trivial finite 1 -element set
C \/ {C} is non empty set
O . (succ C) is set
C is epsilon-transitive epsilon-connected ordinal ordinal-membered set
O . C is set
C is epsilon-transitive epsilon-connected ordinal ordinal-membered set
A . C is set
B is epsilon-transitive epsilon-connected ordinal ordinal-membered set
A . B is set
O . C is set
len (O . C) is epsilon-transitive epsilon-connected ordinal cardinal ordinal-membered set
O . B is set
len (O . B) is epsilon-transitive epsilon-connected ordinal cardinal ordinal-membered set
O is T-Sequence-like Relation-like Function-like () ( {} ) set
O . {} is set
proj1 O is epsilon-transitive epsilon-connected ordinal ordinal-membered set
(O) is set
union (proj1 O) is epsilon-transitive epsilon-connected ordinal ordinal-membered set
O . (union (proj1 O)) is set
A is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal ordinal-membered set
union A is epsilon-transitive epsilon-connected ordinal ordinal-membered set
B is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal ordinal-membered set
B + 1 is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V8() non empty epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative finite cardinal real V70() ordinal-membered Element of NAT
succ B is non empty epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative finite cardinal ordinal-membered set
{B} is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered non empty trivial finite V53() 1 -element set
B \/ {B} is non empty finite set
O . (union A) is set
F1() is T-Sequence-like Relation-like Function-like () ( {} ) set
F1() . {} is set
F2((F1() . {})) is set
proj1 F1() is epsilon-transitive epsilon-connected ordinal ordinal-membered set
O is T-Sequence-like Relation-like Function-like () ( {} ) set
proj1 O is epsilon-transitive epsilon-connected ordinal ordinal-membered set
O | NAT is T-Sequence-like Relation-like proj2 O -valued Function-like () ( {} ) set
proj2 O is set
proj1 (O | NAT) is epsilon-transitive epsilon-connected ordinal ordinal-membered set
((O | NAT)) is epsilon-transitive epsilon-connected ordinal ordinal-membered set
((O | NAT)) is epsilon-transitive epsilon-connected ordinal ordinal-membered set
((O | NAT)) is epsilon-transitive epsilon-connected ordinal ordinal-membered set
((O | NAT)) -^ ((O | NAT)) is epsilon-transitive epsilon-connected ordinal ordinal-membered set
(O | NAT) . {} is set
O . {} is set
C is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal ordinal-membered set
(O | NAT) . C is set
C + 1 is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V8() non empty epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative finite cardinal real V70() ordinal-membered Element of NAT
(O | NAT) . (C + 1) is set
succ C is non empty epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative finite cardinal ordinal-membered set
{C} is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered non empty trivial finite V53() 1 -element set
C \/ {C} is non empty finite set
O . C is set
(O | NAT) . (succ C) is set
O . (succ C) is set
F1() . C is set
F2((F1() . C)) is set
F1() . (succ C) is set
F2((F1() . (succ C))) is set
C is epsilon-transitive epsilon-connected ordinal ordinal-membered set
succ C is non empty epsilon-transitive epsilon-connected ordinal ordinal-membered set
{C} is non empty trivial finite 1 -element set
C \/ {C} is non empty set
(O | NAT) . (succ C) is set
(O | NAT) . C is set
B is epsilon-transitive epsilon-connected ordinal natural ext-real non negative finite cardinal ordinal-membered set
(O | NAT) . B is set
O . C is set
O . (succ C) is set
F1() . C is set
F2((F1() . C)) is set
F1() . (succ C) is set
F2((F1() . (succ C))) is set
O is set
A is Relation-like O -defined Function-like set
C is set
B is set
Swap (A,C,B) is Relation-like Function-like set
proj1 (Swap (A,C,B)) is set
dom A is Element of bool O
bool O is non empty set
O is set
A is Relation-like O -valued Function-like set
C is set
B is set
Swap (A,C,B) is Relation-like Function-like set
proj2 (Swap (A,C,B)) is set
proj2 A is set
O is set
A is set
C is Relation-like Function-like set
proj1 C is set
Swap (C,O,A) is Relation-like Function-like set
(Swap (C,O,A)) . O is set
C . A is set
C +* (O,(C . A)) is Relation-like Function-like set
C . O is set
(C +* (O,(C . A))) +* (A,(C . O)) is Relation-like Function-like set
proj1 (C +* (O,(C . A))) is set
(C +* (O,(C . A))) . O is set
O is set
A is set
C is set
B is Relation-like O -valued Function-like () set
proj1 B is ordinal-membered set
Swap (B,A,C) is Relation-like O -valued Function-like set
(Swap (B,A,C)) /. A is Element of O
B /. C is Element of O
proj1 (Swap (B,A,C)) is set
(Swap (B,A,C)) . A is set
B . C is set
O is set
A is set
C is Relation-like Function-like set
proj1 C is set
Swap (C,O,A) is Relation-like Function-like set
(Swap (C,O,A)) . A is set
C . O is set
C . A is set
C +* (O,(C . A)) is Relation-like Function-like set
(C +* (O,(C . A))) +* (A,(C . O)) is Relation-like Function-like set
proj1 (C +* (O,(C . A))) is set
O is set
A is set
C is set
B is Relation-like O -valued Function-like () set
proj1 B is ordinal-membered set
Swap (B,A,C) is Relation-like O -valued Function-like set
(Swap (B,A,C)) /. C is Element of O
B /. A is Element of O
proj1 (Swap (B,A,C)) is set
(Swap (B,A,C)) . C is set
B . A is set
O is set
A is set
C is set
B is Relation-like Function-like set
Swap (B,A,C) is Relation-like Function-like set
(Swap (B,A,C)) . O is set
B . O is set
proj1 B is set
B . C is set
B +* (A,(B . C)) is Relation-like Function-like set
B . A is set
(B +* (A,(B . C))) +* (C,(B . A)) is Relation-like Function-like set
(B +* (A,(B . C))) . O is set
proj1 B is set
proj1 B is set
O is set
A is set
C is set
B is set
c5 is Relation-like O -valued Function-like () set
proj1 c5 is ordinal-membered set
Swap (c5,C,B) is Relation-like O -valued Function-like set
(Swap (c5,C,B)) /. A is Element of O
c5 /. A is Element of O
proj1 (Swap (c5,C,B)) is set
(Swap (c5,C,B)) . A is set
c5 . A is set
O is set
A is set
C is Relation-like Function-like set
proj1 C is set
Swap (C,O,A) is Relation-like Function-like set
Swap (C,A,O) is Relation-like Function-like set
proj1 (Swap (C,O,A)) is set
proj1 (Swap (C,A,O)) is set
B is set
(Swap (C,O,A)) . B is set
(Swap (C,A,O)) . B is set
(Swap (C,O,A)) . B is set
C . A is set
(Swap (C,A,O)) . B is set
(Swap (C,O,A)) . B is set
C . O is set
(Swap (C,A,O)) . B is set
(Swap (C,O,A)) . B is set
C . B is set
(Swap (C,A,O)) . B is set
O is non empty set
id O is non empty Relation-like O -defined O -valued Function-like one-to-one total quasi_total onto bijective Element of bool [:O,O:]
[:O,O:] is non empty Relation-like set
bool [:O,O:] is non empty set
O is non empty set
A is non empty Relation-like O -valued Function-like onto set
proj1 A is non empty set
C is Element of proj1 A
B is Element of proj1 A
Swap (A,C,B) is Relation-like O -valued Function-like set
proj2 (Swap (A,C,B)) is set
proj2 A is non empty set
O is Relation-like Function-like () set
A is set
C is set
Swap (O,A,C) is Relation-like Function-like set
proj1 O is ordinal-membered set
B is epsilon-transitive epsilon-connected ordinal ordinal-membered set
c5 is epsilon-transitive epsilon-connected ordinal ordinal-membered set
B \ c5 is ordinal-membered Element of bool B
bool B is non empty set
proj1 (Swap (O,A,C)) is set
O is set
A is set
C is Relation-like Function-like () set
proj1 C is ordinal-membered set
Swap (C,O,A) is Relation-like Function-like () set
Swap ((Swap (C,O,A)),O,A) is Relation-like Function-like () set
proj1 (Swap ((Swap (C,O,A)),O,A)) is ordinal-membered set
proj1 (Swap (C,O,A)) is ordinal-membered set
f is set
(Swap ((Swap (C,O,A)),O,A)) . f is set
(Swap (C,O,A)) . f is set
C . f is set
(Swap ((Swap (C,O,A)),O,A)) . f is set
(Swap (C,O,A)) . A is set
C . f is set
(Swap ((Swap (C,O,A)),O,A)) . f is set
(Swap (C,O,A)) . O is set
C . f is set
O is Relation-like Function-like complex-valued ext-real-valued real-valued () set
A is set
C is set
Swap (O,A,C) is Relation-like Function-like () set
B is Relation-like Function-like () set
c5 is set
proj1 B is ordinal-membered set
B . c5 is set
proj1 O is ordinal-membered set
O . C is V8() ext-real real set
O . A is V8() ext-real real set
O . c5 is V8() ext-real real set
O is Relation-like Function-like () set
proj1 O is ordinal-membered set
[:(proj1 O),(proj1 O):] is Relation-like set
bool [:(proj1 O),(proj1 O):] is non empty set
id (proj1 O) is Relation-like proj1 O -defined proj1 O -valued Function-like one-to-one total quasi_total onto bijective Element of bool [:(proj1 O),(proj1 O):]
(id (proj1 O)) * O is Relation-like proj1 O -defined Function-like set
O is Relation-like Function-like () set
proj1 O is ordinal-membered set
proj2 O is set
A is Relation-like Function-like () (O)
proj1 A is ordinal-membered set
proj2 A is set
[:(proj1 O),(proj1 O):] is Relation-like set
bool [:(proj1 O),(proj1 O):] is non empty set
C is Relation-like proj1 O -defined proj1 O -valued Function-like one-to-one total quasi_total onto bijective Element of bool [:(proj1 O),(proj1 O):]
C * O is Relation-like proj1 O -defined Function-like set
proj2 C is set
dom C is Element of bool (proj1 O)
bool (proj1 O) is non empty set
O is Relation-like Function-like () set
proj1 O is ordinal-membered set
id (proj1 O) is Relation-like proj1 O -defined proj1 O -valued Function-like one-to-one total quasi_total onto bijective Element of bool [:(proj1 O),(proj1 O):]
[:(proj1 O),(proj1 O):] is Relation-like set
bool [:(proj1 O),(proj1 O):] is non empty set
(id (proj1 O)) * O is Relation-like proj1 O -defined Function-like set
O is Relation-like Function-like () set
A is Relation-like Function-like () set
proj1 O is ordinal-membered set
proj1 A is ordinal-membered set
[:(proj1 A),(proj1 A):] is Relation-like set
bool [:(proj1 A),(proj1 A):] is non empty set
C is Relation-like proj1 A -defined proj1 A -valued Function-like one-to-one total quasi_total onto bijective Element of bool [:(proj1 A),(proj1 A):]
C * A is Relation-like proj1 A -defined Function-like set
[:(proj1 O),(proj1 O):] is Relation-like set
bool [:(proj1 O),(proj1 O):] is non empty set
C " is Relation-like proj1 A -defined proj1 A -valued Function-like one-to-one total quasi_total onto bijective Element of bool [:(proj1 A),(proj1 A):]
B is Relation-like proj1 O -defined proj1 O -valued Function-like one-to-one total quasi_total onto bijective Element of bool [:(proj1 O),(proj1 O):]
B * O is Relation-like proj1 O -defined Function-like set
id (proj1 A) is Relation-like proj1 A -defined proj1 A -valued Function-like one-to-one total quasi_total onto bijective Element of bool [:(proj1 A),(proj1 A):]
(id (proj1 A)) * A is Relation-like proj1 A -defined Function-like set
C * B is Relation-like proj1 O -defined proj1 A -valued Function-like one-to-one Element of bool [:(proj1 O),(proj1 A):]
[:(proj1 O),(proj1 A):] is Relation-like set
bool [:(proj1 O),(proj1 A):] is non empty set
(C * B) * A is Relation-like proj1 O -defined Function-like set
O is Relation-like Function-like () set
A is Relation-like Function-like () set
C is Relation-like Function-like () set
proj1 C is ordinal-membered set
proj1 A is ordinal-membered set
[:(proj1 A),(proj1 A):] is Relation-like set
bool [:(proj1 A),(proj1 A):] is non empty set
B is Relation-like proj1 A -defined proj1 A -valued Function-like one-to-one total quasi_total onto bijective Element of bool [:(proj1 A),(proj1 A):]
B * A is Relation-like proj1 A -defined Function-like set
[:(proj1 C),(proj1 C):] is Relation-like set
bool [:(proj1 C),(proj1 C):] is non empty set
c5 is Relation-like proj1 C -defined proj1 C -valued Function-like one-to-one total quasi_total onto bijective Element of bool [:(proj1 C),(proj1 C):]
c5 * C is Relation-like proj1 C -defined Function-like set
c5 * B is Relation-like proj1 A -defined proj1 C -valued Function-like one-to-one Element of bool [:(proj1 A),(proj1 C):]
[:(proj1 A),(proj1 C):] is Relation-like set
bool [:(proj1 A),(proj1 C):] is non empty set
f is Relation-like proj1 C -defined proj1 C -valued Function-like one-to-one total quasi_total onto bijective Element of bool [:(proj1 C),(proj1 C):]
f * C is Relation-like proj1 C -defined Function-like set
O is set
id O is Relation-like O -defined O -valued Function-like one-to-one total quasi_total onto bijective Element of bool [:O,O:]
[:O,O:] is Relation-like set
bool [:O,O:] is non empty set
A is set
C is set
Swap ((id O),A,C) is Relation-like O -defined O -valued Function-like set
dom (id O) is Element of bool O
bool O is non empty set
f is set
proj1 (Swap ((id O),A,C)) is set
(Swap ((id O),A,C)) . f is set
k is set
(Swap ((id O),A,C)) . k is set
dom (Swap ((id O),A,C)) is Element of bool O
(id O) . f is set
(id O) . k is set
(id O) . A is set
(id O) . C is set
O is non empty set
id O is non empty Relation-like O -defined O -valued Function-like one-to-one total quasi_total onto bijective Element of bool [:O,O:]
[:O,O:] is non empty Relation-like set
bool [:O,O:] is non empty set
A is Element of O
C is Element of O
Swap ((id O),A,C) is Relation-like O -defined O -valued Function-like set
O is non empty set
id O is non empty Relation-like O -defined O -valued Function-like one-to-one total quasi_total onto bijective Element of bool [:O,O:]
[:O,O:] is non empty Relation-like set
bool [:O,O:] is non empty set
A is Element of O
C is Element of O
Swap ((id O),A,C) is Relation-like O -defined O -valued Function-like one-to-one set
dom (id O) is non empty Element of bool O
bool O is non empty set
B is Element of dom (id O)
c5 is Element of dom (id O)
Swap ((id O),B,c5) is Relation-like O -defined O -valued Function-like one-to-one onto set
dom (Swap ((id O),A,C)) is Element of bool O
O is non empty set
A is non empty set
[:O,A:] is non empty Relation-like set
bool [:O,A:] is non empty set
C is non empty Relation-like O -defined A -valued Function-like total quasi_total Element of bool [:O,A:]
B is Element of O
c5 is Element of O
Swap (C,B,c5) is Relation-like O -defined A -valued Function-like set
dom C is non empty Element of bool O
bool O is non empty set
dom (Swap (C,B,c5)) is Element of bool O
proj2 (Swap (C,B,c5)) is set
proj2 C is non empty set
O is set
A is set
id A is Relation-like A -defined A -valued Function-like one-to-one total quasi_total onto bijective Element of bool [:A,A:]
[:A,A:] is Relation-like set
bool [:A,A:] is non empty set
C is set
Swap ((id A),O,C) is Relation-like A -defined A -valued Function-like set
B is Relation-like Function-like set
c5 is Relation-like Function-like () set
proj1 c5 is ordinal-membered set
Swap (c5,O,C) is Relation-like Function-like () set
B * c5 is Relation-like Function-like set
dom (id A) is Element of bool A
bool A is non empty set
proj2 (id A) is set
proj1 B is set
proj2 B is set
proj1 (Swap (c5,O,C)) is ordinal-membered set
proj1 (B * c5) is set
f is set
(id A) . O is set
(id A) . C is set
(id A) . f is set
(Swap (c5,O,C)) . f is set
c5 . C is set
B . f is set
c5 . O is set
c5 . f is set
(B * c5) . f is set
O is set
A is set
C is Relation-like Function-like () set
proj1 C is ordinal-membered set
Swap (C,O,A) is Relation-like Function-like () set
c5 is non empty set
[:(proj1 C),(proj1 C):] is Relation-like set
bool [:(proj1 C),(proj1 C):] is non empty set
id c5 is non empty Relation-like c5 -defined c5 -valued Function-like one-to-one total quasi_total onto bijective Element of bool [:c5,c5:]
[:c5,c5:] is non empty Relation-like set
bool [:c5,c5:] is non empty set
f is Element of c5
k is Element of c5
(c5,c5,(id c5),f,k) is non empty Relation-like c5 -defined c5 -valued Function-like one-to-one total quasi_total onto bijective Element of bool [:c5,c5:]
f is Relation-like proj1 C -defined proj1 C -valued Function-like one-to-one total quasi_total onto bijective Element of bool [:(proj1 C),(proj1 C):]
f * C is Relation-like proj1 C -defined Function-like set
O is set
A is set
C is Relation-like Function-like () set
proj1 C is ordinal-membered set
Swap (C,O,A) is Relation-like Function-like () set
B is Relation-like Function-like () set
Swap (B,O,A) is Relation-like Function-like () set
proj1 B is ordinal-membered set
O is RelStr
the carrier of O is set
A is Relation-like the carrier of O -valued Function-like () set
proj1 A is ordinal-membered set
{ [b1,b2] where b1, b2 is epsilon-transitive epsilon-connected ordinal ordinal-membered Element of proj1 A : ( b1 in b2 & not A /. b1 <= A /. b2 ) } is set
O is RelStr
the carrier of O is set
A is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V7() empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural Relation-like non-empty empty-yielding NAT -defined the carrier of O -valued Function-like one-to-one constant functional ext-real non positive non negative complex-valued ext-real-valued real-valued natural-valued finite finite-yielding V53() cardinal {} -element Ordinal-yielding increasing V67() V71() decreasing non-decreasing non-increasing V79() ordinal-membered () ( {} ) set
C is epsilon-transitive epsilon-connected ordinal ordinal-membered set
proj1 A is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V7() empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional ext-real non positive non negative complex-valued ext-real-valued real-valued natural-valued finite finite-yielding V53() cardinal {} -element Ordinal-yielding increasing V67() V71() decreasing non-decreasing non-increasing V79() ordinal-membered () ( {} ) set
A /. C is Element of the carrier of O
B is epsilon-transitive epsilon-connected ordinal ordinal-membered set
A /. B is Element of the carrier of O
A is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V7() empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural Relation-like non-empty empty-yielding NAT -defined the carrier of O -valued the carrier of O -valued Function-like one-to-one constant functional ext-real non positive non negative complex-valued ext-real-valued real-valued natural-valued finite finite-yielding V53() cardinal {} -element Ordinal-yielding increasing V67() V71() decreasing non-decreasing non-increasing V79() ordinal-membered () ( {} ) (O) set
(O,A) is set
proj1 A is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V7() empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional ext-real non positive non negative complex-valued ext-real-valued real-valued natural-valued finite finite-yielding V53() cardinal {} -element Ordinal-yielding increasing V67() V71() decreasing non-decreasing non-increasing V79() ordinal-membered () ( {} ) set
{ [b1,b2] where b1, b2 is epsilon-transitive epsilon-connected ordinal ordinal-membered Element of proj1 A : ( b1 in b2 & not A /. b1 <= A /. b2 ) } is set
the Element of (O,A) is Element of (O,A)
dom A is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V7() empty proper epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural Relation-like non-empty empty-yielding NAT -defined RAT -valued Function-like one-to-one constant functional ext-real non positive non negative complex-valued ext-real-valued real-valued natural-valued finite finite-yielding V53() cardinal {} -element Ordinal-yielding increasing V67() V71() decreasing non-decreasing non-increasing V79() ordinal-membered () ( {} ) Element of bool NAT
B is V8() epsilon-transitive epsilon-connected ordinal natural Relation-like Function-like ext-real non negative finite cardinal real V70() ordinal-membered Element of dom A
c5 is V8() epsilon-transitive epsilon-connected ordinal natural Relation-like Function-like ext-real non negative finite cardinal real V70() ordinal-membered Element of dom A
[B,c5] is V30() set
{B,c5} is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered non empty functional finite V53() set
{B} is complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered non empty trivial functional finite V53() 1 -element V90() set
{{B,c5},{B}} is non empty finite V53() set
A /. B is Element of the carrier of O
A /. c5 is Element of the carrier of O
O is non empty reflexive transitive antisymmetric connected RelStr
the carrier of O is non empty set
C is Element of the carrier of O
A is Element of the carrier of O
O is non empty reflexive transitive antisymmetric connected RelStr
the carrier of O is non empty set
A is Relation-like the carrier of O -valued Function-like () set
(O,A) is set
proj1 A is ordinal-membered set
{ [b1,b2] where b1, b2 is epsilon-transitive epsilon-connected ordinal ordinal-membered Element of proj1 A : ( b1 in b2 & not A /. b1 <= A /. b2 ) } is set
{ [b1,b2] where b1, b2 is epsilon-transitive epsilon-connected ordinal ordinal-membered Element of proj1 A : ( b1 in b2 & A /. b2 < A /. b1 ) } is set
B is set
c5 is epsilon-transitive epsilon-connected ordinal ordinal-membered Element of proj1 A
f is epsilon-transitive epsilon-connected ordinal ordinal-membered Element of proj1 A
[c5,f] is V30() set
{c5,f} is non empty finite set
{c5} is non empty trivial finite 1 -element set
{{c5,f},{c5}} is non empty finite V53() set
A /. c5 is Element of the carrier of O
A /. f is Element of the carrier of O
B is set
c5 is epsilon-transitive epsilon-connected ordinal ordinal-membered Element of proj1 A
f is epsilon-transitive epsilon-connected ordinal ordinal-membered Element of proj1 A
[c5,f] is V30() set
{c5,f} is non empty finite set
{c5} is non empty trivial finite 1 -element set
{{c5,f},{c5}} is non empty finite V53() set
A /. f is Element of the carrier of O
A /. c5 is Element of the carrier of O
B is set
c5 is set
O is set
A is set
[O,A] is V30() set
{O,A} is non empty finite set
{O} is non empty trivial finite 1 -element set
{{O,A},{O}} is non empty finite V53() set
C is non empty reflexive transitive antisymmetric connected RelStr
the carrier of C is non empty set
B is Relation-like the carrier of C -valued Function-like () set
(C,B) is set
proj1 B is ordinal-membered set
{ [b1,b2] where b1, b2 is epsilon-transitive epsilon-connected ordinal ordinal-membered Element of proj1 B : ( b1 in b2 & not B /. b1 <= B /. b2 ) } is set
{ [b1,b2] where b1, b2 is epsilon-transitive epsilon-connected ordinal ordinal-membered Element of proj1 B : ( b1 in b2 & B /. b2 < B /. b1 ) } is set
B /. A is Element of the carrier of C
B /. O is Element of the carrier of C
c5 is non empty Relation-like Function-like set
proj1 c5 is non empty set
f is Element of proj1 c5
k is Element of proj1 c5
[f,k] is V30() set
{f,k} is non empty finite set
{f} is non empty trivial finite 1 -element set
{{f,k},{f}} is non empty finite V53() set
B /. f is Element of the carrier of C
B /. k is Element of the carrier of C
O is non empty reflexive transitive antisymmetric connected RelStr
the carrier of O is non empty set
A is Relation-like the carrier of O -valued Function-like () set
(O,A) is set
proj1 A is ordinal-membered set
{ [b1,b2] where b1, b2 is epsilon-transitive epsilon-connected ordinal ordinal-membered Element of proj1 A : ( b1 in b2 & not A /. b1 <= A /. b2 ) } is set
{ [b1,b2] where b1, b2 is epsilon-transitive epsilon-connected ordinal ordinal-membered Element of proj1 A : ( b1 in b2 & A /. b2 < A /. b1 ) } is set
[:(proj1 A),(proj1 A):] is Relation-like set
C is set
B is epsilon-transitive epsilon-connected ordinal ordinal-membered Element of proj1 A
c5 is epsilon-transitive epsilon-connected ordinal ordinal-membered Element of proj1 A
[B,c5] is V30() set
{B,c5} is non empty finite set
{B} is non empty trivial finite 1 -element set
{{B,c5},{B}} is non empty finite V53() set
A /. c5 is Element of the carrier of O
A /. B is Element of the carrier of O
O is non empty reflexive transitive antisymmetric connected RelStr
the carrier of O is non empty set
A is Relation-like the carrier of O -valued Function-like finite () set
(O,A) is set
proj1 A is finite ordinal-membered set
{ [b1,b2] where b1, b2 is epsilon-transitive epsilon-connected ordinal ordinal-membered Element of proj1 A : ( b1 in b2 & not A /. b1 <= A /. b2 ) } is set
{ [b1,b2] where b1, b2 is epsilon-transitive epsilon-connected ordinal ordinal-membered Element of proj1 A : ( b1 in b2 & A /. b2 < A /. b1 ) } is set
[:(proj1 A),(proj1 A):] is Relation-like finite set
O is non empty reflexive transitive antisymmetric connected RelStr
the carrier of O is non empty set
A is Relation-like the carrier of O -valued Function-like () set
(O,A) is set
proj1 A is ordinal-membered set
{ [b1,b2] where b1, b2 is epsilon-transitive epsilon-connected ordinal ordinal-membered Element of proj1 A : ( b1 in b2 & not A /. b1 <= A /. b2 ) } is set
{ [b1,b2] where b1, b2 is epsilon-transitive epsilon-connected ordinal ordinal-membered Element of proj1 A : ( b1 in b2 & A /. b2 < A /. b1 ) } is set
the Element of (O,A) is Element of (O,A)
B is epsilon-transitive epsilon-connected ordinal ordinal-membered Element of proj1 A
c5 is epsilon-transitive epsilon-connected ordinal ordinal-membered Element of proj1 A
[B,c5] is V30() set
{B,c5} is non empty finite set
{B} is non empty trivial finite 1 -element set
{{B,c5},{B}} is non empty finite V53() set
A /. c5 is Element of the carrier of O
A /. B is Element of the carrier of O
C is epsilon-transitive epsilon-connected ordinal ordinal-membered set
A /. C is Element of the carrier of O
B is epsilon-transitive epsilon-connected ordinal ordinal-membered set
A /. B is Element of the carrier of O
[C,B] is V30() set
{C,B} is non empty finite set
{C} is non empty trivial finite 1 -element set
{{C,B},{C}} is non empty finite V53() set
O is set
A is set
[O,A] is V30() set
{O,A} is non empty finite set
{O} is non empty trivial finite 1 -element set
{{O,A},{O}} is non empty finite V53() set
[A,O] is V30() set
{A,O} is non empty finite set
{A} is non empty trivial finite 1 -element set
{{A,O},{A}} is non empty finite V53() set
C is non empty reflexive transitive antisymmetric connected RelStr
the carrier of C is non empty set
B is Relation-like the carrier of C -valued Function-like () set
(C,B) is set
proj1 B is ordinal-membered set
{ [b1,b2] where b1, b2 is epsilon-transitive epsilon-connected ordinal ordinal-membered Element of proj1 B : ( b1 in b2 & not B /. b1 <= B /. b2 ) } is set
{ [b1,b2] where b1, b2 is epsilon-transitive epsilon-connected ordinal ordinal-membered Element of proj1 B : ( b1 in b2 & B /. b2 < B /. b1 ) } is set
O is set
A is set
[O,A] is V30() set
{O,A} is non empty finite set
{O} is non empty trivial finite 1 -element set
{{O,A},{O}} is non empty finite V53() set
C is set
[A,C] is V30() set
{A,C} is non empty finite set
{A} is non empty trivial finite 1 -element set
{{A,C},{A}} is non empty finite V53() set
[O,C] is V30() set
{O,C} is non empty finite set
{{O,C},{O}} is non empty finite V53() set
B is non empty reflexive transitive antisymmetric connected RelStr
the carrier of B is non empty set
c5 is Relation-like the carrier of B -valued Function-like () set
(B,c5) is set
proj1 c5 is ordinal-membered set
{ [b1,b2] where b1, b2 is epsilon-transitive epsilon-connected ordinal ordinal-membered Element of proj1 c5 : ( b1 in b2 & not c5 /. b1 <= c5 /. b2 ) } is set
{ [b1,b2] where b1, b2 is epsilon-transitive epsilon-connected ordinal ordinal-membered Element of proj1 c5 : ( b1 in b2 & c5 /. b2 < c5 /. b1 ) } is set
f is epsilon-transitive epsilon-connected ordinal ordinal-membered Element of proj1 c5
k is epsilon-transitive epsilon-connected ordinal ordinal-membered Element of proj1 c5
c5 /. k is Element of the carrier of B
c5 /. f is Element of the carrier of B
f is epsilon-transitive epsilon-connected ordinal ordinal-membered Element of proj1 c5
c5 /. f is Element of the carrier of B
O is non empty reflexive transitive antisymmetric connected RelStr
the carrier of O is non empty set
A is Relation-like the carrier of O -valued Function-like () set
(O,A) is set
proj1 A is ordinal-membered set
{ [b1,b2] where b1, b2 is epsilon-transitive epsilon-connected ordinal ordinal-membered Element of proj1 A : ( b1 in b2 & not A /. b1 <= A /. b2 ) } is set
{ [b1,b2] where b1, b2 is epsilon-transitive epsilon-connected ordinal ordinal-membered Element of proj1 A : ( b1 in b2 & A /. b2 < A /. b1 ) } is set
[:(proj1 A),(proj1 A):] is Relation-like set
O is non empty reflexive transitive antisymmetric connected RelStr
the carrier of O is non empty set
A is Relation-like the carrier of O -valued Function-like () set
(O,A) is Relation-like set
proj1 A is ordinal-membered set
{ [b1,b2] where b1, b2 is epsilon-transitive epsilon-connected ordinal ordinal-membered Element of proj1 A : ( b1 in b2 & not A /. b1 <= A /. b2 ) } is set
{ [b1,b2] where b1, b2 is epsilon-transitive epsilon-connected ordinal ordinal-membered Element of proj1 A : ( b1 in b2 & A /. b2 < A /. b1 ) } is set
C is Relation-like set
B is set
field C is set
proj1 C is set
proj2 C is set
(proj1 C) \/ (proj2 C) is set
c5 is set
[B,c5] is V30() set
{B,c5} is non empty finite set
{B} is non empty trivial finite 1 -element set
{{B,c5},{B}} is non empty finite V53() set
[c5,B] is V30() set
{c5,B} is non empty finite set
{c5} is non empty trivial finite 1 -element set
{{c5,B},{c5}} is non empty finite V53() set
B is set
field C is set
proj1 C is set
proj2 C is set
(proj1 C) \/ (proj2 C) is set
c5 is