:: EXCHSORT semantic presentation

bool REAL is non empty set

bool NAT is non empty non trivial non finite set
bool NAT is non empty non trivial non finite set

K158(NAT,0,1) ^omega is non empty functional set
bool (K158(NAT,0,1) ^omega) is non empty set

bool is non empty set
K326() is 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

bool [:K452(K453()),NAT:] is non empty set

bool [:NAT,K452(K453()):] is non empty set

K317(2,K326()) is M14(K326())
[:K317(2,K326()),K326():] is Relation-like set
bool [:K317(2,K326()),K326():] is non empty set

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():]

(O +^ A) \ O is ordinal-membered Element of bool (O +^ A)
bool (O +^ A) is non empty set
C is 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

proj1 O is 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 \ A is ordinal-membered Element of bool O
bool O is non empty set

On (O \ A) is ordinal-membered set
K181((On (O \ A))) is set

B is set
c5 is set

O \ A is ordinal-membered Element of bool O
bool O is non empty set

f is set
c5 . f is set
k is set
c5 . k is set

c5 . f is set

c5 . c9 is set

proj2 c5 is set

f is set
k is set
c5 . k is set

proj1 O is set

proj1 A is set

C \ B is ordinal-membered Element of bool C
bool C is non empty set

proj1 O is set

A \ C is ordinal-membered Element of bool A
bool A is non empty set

proj1 O is set
() \ {} is ordinal-membered Element of bool ()
bool () is non empty set

proj1 O is set

bool C is non empty finite V53() set
f is set

k is set

proj1 A is set

C \ B is ordinal-membered Element of bool C
bool C is non empty set

O \ O is ordinal-membered Element of bool O
bool O is non empty set

C \ O is ordinal-membered Element of bool C
bool C is non empty set

proj1 A is set

C \ B is ordinal-membered Element of bool C
bool C is non empty set

O \ f is ordinal-membered Element of bool O
bool O is non empty set

O \ C is ordinal-membered Element of bool O
bool O is non empty set

proj1 O is set

proj1 O is set

proj1 O is set

K181((On ())) is set

proj1 O is set

proj1 C is set

proj1 O is set

K181((On ())) is set

proj1 O is set

A is set

proj1 O is set

C is set
A is set

[:C,A:] is Relation-like set
bool [:C,A:] is non empty set

proj1 O is set

A \ C is ordinal-membered Element of bool A
bool A is non empty set

A \ C is ordinal-membered Element of bool A
bool A is non empty set

proj1 O is set

K181((On ())) is set

proj1 O is set

K181((On ())) is set

(O) \ (O) is ordinal-membered Element of bool (O)
bool (O) is non empty set

A \ C is ordinal-membered Element of bool A
bool A is non empty set

K181((On ())) is set
B is set
B is set

O \ A is ordinal-membered Element of bool O
bool O is non empty set

() \ {} is ordinal-membered Element of bool ()
bool () is non empty set

C 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

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,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

proj2 C is 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

proj2 C is set

A is non empty 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

proj2 B is set
{C} is non empty trivial finite 1 -element 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 \/ {O} is non empty set

[] is V30() set
{} is non empty finite set
{O} is non empty trivial finite 1 -element set
{{},{O}} is non empty finite V53() set

O \/ {O} is non empty 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

O \/ {O} is non empty set

O . (union ()) is set

last O is set

O . (union ()) is set
(O) is set

O . A is set

O . C is set

B \ c5 is ordinal-membered Element of bool B
bool B is non empty set

c9 \/ {c9} is non empty finite set

{A} is non empty trivial finite 1 -element set
A \/ {A} is non empty set

O . H1( {} ) is set

O . H1(b) is set

O . H1(b + 1) is set

b \/ {b} is non empty finite set

{((succ A) +^ b)} is non empty trivial finite 1 -element set
((succ A) +^ b) \/ {((succ A) +^ b)} is non empty set

O . A is set

O . C is set

B \ c5 is ordinal-membered Element of bool B
bool B is non empty set

f \/ {f} is non empty finite set

{A} is non empty trivial finite 1 -element set
A \/ {A} is non empty set

O . H1( {} ) is set

O . H1(y) is set

O . H1(y + 1) is set

y \/ {y} is non empty finite set

{((succ A) +^ y)} is non empty trivial finite 1 -element set
((succ A) +^ y) \/ {((succ A) +^ y)} is non empty set

O . {} is set

O . C is set

{C} is non empty trivial finite 1 -element set
C \/ {C} is non empty set
O . (succ C) is set

O . C is set

A . C is set

A . B is set
O . C is set

O . B is set

O . {} is set

(O) is set

O . (union ()) is set

B \/ {B} is non empty finite set
O . () is set
F1() is T-Sequence-like Relation-like Function-like () ( {} ) set
F1() . {} is set
F2((F1() . {})) is set

proj2 O is set

(O | NAT) . {} is set
O . {} is set

(O | NAT) . C is set

(O | NAT) . (C + 1) is 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 non empty trivial finite 1 -element set
C \/ {C} is non empty set
(O | NAT) . (succ C) is set
(O | NAT) . C is 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

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

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

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

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

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

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

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

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

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

[:O,O:] is non empty Relation-like set
bool [:O,O:] is non empty set
O is non empty 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

A is set
C is set
Swap (O,A,C) is Relation-like Function-like 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

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

A is set
C is set
Swap (O,A,C) is Relation-like Function-like () set

c5 is set

B . c5 is 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

[:(),():] is Relation-like set
bool [:(),():] is non empty set

proj2 O is set
A is Relation-like Function-like () (O)

proj2 A is set
[:(),():] is Relation-like set
bool [:(),():] is non empty set

proj2 C is set
dom C is Element of bool ()
bool () is non empty set

[:(),():] is Relation-like set
bool [:(),():] is non empty set

[:(),():] is Relation-like set
bool [:(),():] is non empty set

[:(),():] is Relation-like set
bool [:(),():] is non empty set

[:(),():] is Relation-like set
bool [:(),():] is non empty set

[:(),():] is Relation-like set
bool [:(),():] is non empty set

[:(),():] is Relation-like set
bool [:(),():] is non empty set

[:(),():] is Relation-like set
bool [:(),():] is non empty set

O is set

[: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

[: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

[: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

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

[: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

Swap (c5,O,C) 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

Swap (C,O,A) is Relation-like Function-like () set
c5 is non empty set
[:(),():] is Relation-like set
bool [:(),():] is non empty set

[: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:]

O is set
A is set

Swap (C,O,A) is Relation-like Function-like () set

Swap (B,O,A) is Relation-like Function-like () set

O is RelStr
the carrier of O is set
A is Relation-like the carrier of O -valued Function-like () 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 /. C is Element of the carrier of O

A /. B is Element of the carrier of O

(O,A) is 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)

[B,c5] is V30() 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

the carrier of O is non empty set
C is Element of the carrier of O
A is Element of the carrier of O

the carrier of O is non empty set
A is Relation-like the carrier of O -valued Function-like () set
(O,A) is 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,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,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

the carrier of C is non empty set
B is Relation-like the carrier of C -valued Function-like () set
(C,B) is 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

the carrier of O is non empty set
A is Relation-like the carrier of O -valued Function-like () set
(O,A) is 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
[:(),():] is Relation-like set
C 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
A /. c5 is Element of the carrier of O
A /. B is Element of the carrier of O

the carrier of O is non empty set

(O,A) is 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
[:(),():] is Relation-like finite set

the carrier of O is non empty set
A is Relation-like the carrier of O -valued Function-like () set
(O,A) is 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,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

A /. C is Element of the carrier of O

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

the carrier of C is non empty set
B is Relation-like the carrier of C -valued Function-like () set
(C,B) is 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

the carrier of B is non empty set
c5 is Relation-like the carrier of B -valued Function-like () set
(B,c5) is 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

c5 /. k is Element of the carrier of B
c5 /. f is Element of the carrier of B

c5 /. f is Element of the carrier of B

the carrier of O is non empty set
A is Relation-like the carrier of O -valued Function-like () set
(O,A) is 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
[:(),():] is Relation-like set

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

{ [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
field C is set
proj1 C is set
proj2 C is set
() \/ () 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
() \/ () is set
c5 is