:: ORDINAL1 semantic presentation

{} is empty Relation-like non-empty empty-yielding Function-like one-to-one constant functional set

the empty Relation-like non-empty empty-yielding Function-like one-to-one constant functional set is empty Relation-like non-empty empty-yielding Function-like one-to-one constant functional set

X is set

Y is set

X is set

{X} is non empty set

X \/ {X} is non empty set

X is set

(X) is set

{X} is non empty set

X \/ {X} is non empty set

X is set

(X) is non empty set

{X} is non empty set

X \/ {X} is non empty set

X is set

(X) is non empty set

{X} is non empty set

X \/ {X} is non empty set

Y is set

(Y) is non empty set

{Y} is non empty set

Y \/ {Y} is non empty set

X is set

Y is set

(Y) is non empty set

{Y} is non empty set

Y \/ {Y} is non empty set

X is set

(X) is non empty set

{X} is non empty set

X \/ {X} is non empty set

X is set

X is set

Y is set

X is set

X is set

X is set

Y is set

x is () set

X is () set

Y is () () () set

Y \ X is Element of bool Y

bool Y is non empty set

the Element of Y \ X is Element of Y \ X

y is set

A2 is set

B is set

A2 is set

X is () set

Y is () () () set

x is () () () set

X is set

Y is () () () set

x is set

y is set

x \ X is Element of bool x

bool x is non empty set

A2 is set

x is set

y is set

X is () () () set

Y is () () () set

x is set

X \ Y is Element of bool X

bool X is non empty set

y is set

A2 is set

X is () () () set

Y is () () () set

x is () () () set

x is set

y is () () () set

x is () () () set

y is () () () set

A2 is () () () set

B is () () () set

X is () () () set

Y is () () () set

X is () () () set

Y is () () () set

X is set

X is set

(X) is non empty set

{X} is non empty set

X \/ {X} is non empty set

Y is set

Y is set

Y is set

x is set

X is set

union X is set

x is set

y is set

Y is () () () set

A2 is () () () set

x is set

y is set

A2 is set

Y is () () () set

B is set

A is () () () set

a is () () () set

({}) is non empty set

{{}} is non empty functional set

{} \/ {{}} is non empty set

X is () () () set

X is () () () set

(X) is non empty set

{X} is non empty set

X \/ {X} is non empty set

union X is set

X is set

Y is set

Y is set

x is set

X is set

Y is () () () set

the Element of X is Element of X

y is set

A2 is () () () set

B is () () () set

X is () () () set

(X) is non empty () () () set

{X} is non empty set

X \/ {X} is non empty set

Y is () () () set

x is set

X is () () () set

Y is () () () set

(Y) is non empty () () () set

{Y} is non empty set

Y \/ {Y} is non empty set

X is () () () set

X is () () () set

(X) is non empty () () () set

{X} is non empty set

X \/ {X} is non empty set

Y is set

x is set

x is () () () set

y is () () () set

y is () () () set

X is () () () set

(X) is non empty () () () set

{X} is non empty set

X \/ {X} is non empty set

x is set

(X) \ x is Element of bool (X)

bool (X) is non empty set

y is () () () set

A2 is () () () set

B is () () () set

y is () () () set

X is set

union X is set

Y is set

x is set

y is set

Y is set

x is set

y is set

A2 is set

X is set

union X is set

((union X)) is non empty set

{(union X)} is non empty set

(union X) \/ {(union X)} is non empty set

Y is () () () set

x is set

y is () () () set

A2 is set

X is set

Y is set

x is set

Y is set

x is set

X is set

Y is set

x is set

x is set

y is set

X is set

Y is () () () set

(Y) is non empty () () () set

{Y} is non empty set

Y \/ {Y} is non empty set

x is set

y is set

y is () () () set

A2 is () () () set

X is () () () set

union X is () () () set

Y is () () () set

(Y) is non empty () () () set

{Y} is non empty set

Y \/ {Y} is non empty set

x is set

y is set

Y is set

(Y) is non empty set

{Y} is non empty set

Y \/ {Y} is non empty set

union X is () () () set

Y is set

x is set

X is () () () set

Y is () () () set

(Y) is non empty () () () set

{Y} is non empty set

Y \/ {Y} is non empty set

Y is () () () set

(Y) is non empty () () () set

{Y} is non empty set

Y \/ {Y} is non empty set

X is set

proj1 X is set

X is set

Y is Relation-like Function-like () set

proj2 {} is empty trivial Relation-like non-empty empty-yielding Function-like one-to-one constant functional () () () () set

proj2 Y is set

X is set

Y is Relation-like Function-like () set

proj2 Y is set

X is Relation-like Function-like set

proj1 X is set

proj2 X is set

X is Relation-like Function-like () set

proj1 X is set

X is set

Y is set

x is Relation-like X -valued Function-like () set

proj2 x is set

X is Relation-like Function-like () set

proj2 X is set

Y is () () () set

X | Y is Relation-like Function-like set

proj2 (X | Y) is set

proj1 X is () () () set

proj1 (X | Y) is set

X is set

Y is Relation-like X -valued Function-like () set

x is () () () set

Y | x is Relation-like X -valued proj2 Y -valued Function-like () set

proj2 Y is set

X is set

union X is set

Y is set

x is set

y is Relation-like Function-like () set

A2 is set

Y is set

x is set

[Y,x] is V14() set

{Y,x} is non empty set

{Y} is non empty set

{{Y,x},{Y}} is non empty set

y is set

[Y,y] is V14() set

{Y,y} is non empty set

{{Y,y},{Y}} is non empty set

A2 is set

a is set

A is Relation-like Function-like () set

B is Relation-like Function-like () set

x is set

y is set

A2 is set

B is Relation-like Function-like () set

proj1 B is () () () set

x is Relation-like Function-like set

y is set

A2 is set

[y,A2] is V14() set

{y,A2} is non empty set

{y} is non empty set

{{y,A2},{y}} is non empty set

B is Relation-like Function-like () set

proj1 B is () () () set

proj2 x is set

y is set

proj1 x is set

A2 is set

x . A2 is set

[A2,y] is V14() set

{A2,y} is non empty set

{A2} is non empty set

{{A2,y},{A2}} is non empty set

y is () () () set

A2 is () () () set

A2 is () () () set

Y is Relation-like Function-like set

proj1 Y is set

B is set

a is set

[B,a] is V14() set

{B,a} is non empty set

{B} is non empty set

{{B,a},{B}} is non empty set

A is set

L is Relation-like Function-like () set

proj1 L is () () () set

B is Relation-like Function-like () set

proj1 B is () () () set

[L,(proj1 L)] is V14() set

{L,(proj1 L)} is non empty set

{L} is non empty functional set

{{L,(proj1 L)},{L}} is non empty set

proj1 x is set

x . L is set

B is set

a is () () () set

A is () () () set

proj1 x is set

L is set

x . L is set

[L,A] is V14() set

{L,A} is non empty set

{L} is non empty set

{{L,A},{L}} is non empty set

B is Relation-like Function-like () set

proj1 B is () () () set

A is Relation-like Function-like () set

proj1 A is () () () set

A is Relation-like Function-like () set

proj1 A is () () () set

L is set

[B,L] is V14() set

{B,L} is non empty set

{B} is non empty set

{{B,L},{B}} is non empty set

F

proj1 F

F

F

proj1 F

X is set

Y is set

Y is set

F

F

Y is () () () set

F

proj2 F

proj1 (F

F

proj2 F

proj1 (F

x is () () () set

F

F

x is set

y is () () () set

F

F

(F

F

(F

F

F

F

F

F

X is () () () set

Y is set

x is set

y is set

A2 is Relation-like Function-like () set

proj1 A2 is () () () set

B is () () () set

a is () () () set

A is Relation-like Function-like () set

A2 | a is Relation-like proj2 A2 -valued Function-like () set

proj2 A2 is set

A2 . a is set

F

a is Relation-like Function-like () set

proj1 a is () () () set

A is () () () set

L is Relation-like Function-like () set

a | A is Relation-like proj2 a -valued Function-like () set

proj2 a is set

a . A is set

F

Y is Relation-like Function-like set

proj1 Y is set

x is set

y is set

[x,y] is V14() set

{x,y} is non empty set

{x} is non empty set

{{x,y},{x}} is non empty set

x is set

y is () () () set

A2 is Relation-like Function-like () set

proj1 A2 is () () () set

B is () () () set

a is Relation-like Function-like () set

proj1 a is () () () set

A is () () () set

a . A is set

a | A is Relation-like proj2 a -valued Function-like () set

proj2 a is set

F

[y,A2] is V14() set

{y,A2} is non empty set

{y} is non empty set

{{y,A2},{y}} is non empty set

x is set

Y . x is set

y is set

[x,y] is V14() set

{x,y} is non empty set

{x} is non empty set

{{x,y},{x}} is non empty set

A2 is Relation-like Function-like () set

F

x is set

B is Relation-like Function-like () set

Y . x is set

y is set

F

a is Relation-like Function-like () set

A2 is set

F

x is Relation-like Function-like set

proj1 x is set

y is Relation-like Function-like () set

proj1 y is () () () set

A2 is () () () set

y . A2 is set

y | A2 is Relation-like proj2 y -valued Function-like () set

proj2 y is set

F

Y . A2 is set

x . A2 is set

B is Relation-like Function-like () set

F

[A2,B] is V14() set

{A2,B} is non empty set

{A2} is non empty set

{{A2,B},{A2}} is non empty set

proj1 B is () () () set

a is () () () set

A is () () () set

L is Relation-like Function-like () set

B | a is Relation-like proj2 B -valued Function-like () set

proj2 B is set

proj1 L is () () () set

B is () () () set

B | B is Relation-like proj2 B -valued Function-like () set

L | B is Relation-like proj2 L -valued Function-like () set

proj2 L is set

B . B is set

F

L . B is set

F

[a,(B | a)] is V14() set

{a,(B | a)} is non empty set

{a} is non empty set

{{a,(B | a)},{a}} is non empty set

Y . a is set

a is set

A is () () () set

Y . A is set

B | A is Relation-like proj2 B -valued Function-like () set

(y | A2) . A is set

y . A is set

x . A is set

(y | A2) . a is set

B . a is set

L is Relation-like Function-like () set

F

proj1 (y | A2) is () () () set

X is Relation-like Function-like () set

proj1 X is () () () set

Y is () () () set

X | Y is Relation-like proj2 X -valued Function-like () set

proj2 X is set

X . Y is set

x is Relation-like Function-like () set

F

F

proj1 F

F

X is Relation-like Function-like () set

F

proj1 X is () () () set

Y is set

proj2 X is set

x is () () () set

X | x is Relation-like proj2 X -valued Function-like () set

F

y is Relation-like proj2 X -valued Function-like () set

F

proj1 y is () () () set

A2 is () () () set

X | A2 is Relation-like proj2 X -valued Function-like () set

y | A2 is Relation-like proj2 X -valued proj2 y -valued Function-like () set

proj2 y is set

y . A2 is set

X . A2 is set

F

F

X . x is set

y is Relation-like proj2 X -valued Function-like () set

F

proj1 y is () () () set

F

X . Y is set

Y is () () () set

F

F

proj2 F

F

X is () () () set

Y is () () () set

X is set

Y is set

x is set

Y is set

x is set

X is () () () set

Y is set

(Y) is set

x is set

y is () () () set

A2 is set

B is () () () set

x is () () () set

y is () () () set

(y) is non empty () () () set

{y} is non empty set

y \/ {y} is non empty set

bool y is non empty set

A2 is set

X is () () () set

X is set

Y is set

() is set

the Element of () is Element of ()

X is Element of ()

X is () set

X is () () () set

Y is Element of X

X is set

Y is () () () Element of ()

F

X is set

Y is Element of F

x is () () () set

y is set

A2 is () () () set

X is set

Y is set

x is set

y is () () () set

A2 is () () () set

X is Relation-like Function-like set

proj1 X is set

Y is Element of F

X . Y is set

X is set

(X) is non empty set

{X} is non empty set

X \/ {X} is non empty set

(X) \ {X} is Element of bool (X)

bool (X) is non empty set

Y is set

Y is set

X is set

X is () () () Element of ()

({}) is non empty () () () set

{{}} is non empty functional set

{} \/ {{}} is non empty set

X is () () () () set

(X) is non empty () () () set

{X} is non empty set

X \/ {X} is non empty set

X is set

Y is set

x is set

X is () set

bool X is non empty set

Y is Element of bool X

x is set

y is set