:: STRUCT_0 semantic presentation

K115() is set

K119() is non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal Element of bool K115()

bool K115() is set

omega is non empty non trivial epsilon-transitive epsilon-connected ordinal non finite cardinal limit_cardinal set

bool omega is non empty non trivial non finite set

bool K119() is non empty non trivial non finite set

{} is V6() V9() empty trivial epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural finite V36() cardinal {} -element complex set

the V6() V9() empty trivial epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural finite V36() cardinal {} -element complex set is V6() V9() empty trivial epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural finite V36() cardinal {} -element complex set

1 is non empty epsilon-transitive epsilon-connected ordinal natural finite cardinal complex Element of K119()

{{}} is non empty trivial finite V36() 1 -element set

2 is non empty epsilon-transitive epsilon-connected ordinal natural finite cardinal complex Element of K119()

{{},1} is non empty finite V36() set

({}) is () ()

S is () ()

the of S is set

({{}}) is () ()

the of ({{}}) is set

S is () ()

the of S is set

S is () ()

the of S is set

S is ()

the of S is set

bool the of S is set

{} the of S is Element of bool the of S

[#] the of S is Element of bool the of S

S is ()

(S) is Element of bool the of S

the of S is set

bool the of S is set

S is () ()

(S) is V9() c=-linear finite V36() Element of bool the of S

the of S is V6() V9() empty trivial epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural finite V36() cardinal {} -element complex set

bool the of S is finite V36() set

S is () ()

(S) is Element of bool the of S

the of S is non empty set

bool the of S is set

S is () ()

the of S is non empty set

bool the of S is set

(S) is non empty Element of bool the of S

S is ()

the of S is set

id the of S is Relation-like the of S -defined the of S -valued V6() V7() total V18( the of S, the of S) Element of bool [: the of S, the of S:]

[: the of S, the of S:] is set

bool [: the of S, the of S:] is set

the non empty set is non empty set

the Element of the non empty set is Element of the non empty set

( the non empty set , the Element of the non empty set ) is () ()

the of ( the non empty set , the Element of the non empty set ) is set

S is ()

the of S is Element of the of S

the of S is set

S is ()

the of S is Element of the of S

the of S is set

S is ()

the of S is set

S is ()

S is ()

the of S is set

y is Element of the of S

A is Element of the of S

y is set

A is set

y is Element of the of S

A is Element of the of S

y is Element of the of S

A is Element of the of S

S is ()

(S) is Element of the of S

the of S is set

the of S is Element of the of S

(S) is Element of the of S

the of S is Element of the of S

(1) is () ()

(2) is () ()

S is () ()

the of S is set

X is Element of the of S

y is Element of the of S

S is () () ()

the of S is non empty set

S is () ()

the of S is set

({{}}) is () ()

S is () ()

the of S is set

S is () () ()

the of S is V6() V9() empty trivial epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural finite V36() cardinal {} -element complex set

the non empty non trivial non finite set is non empty non trivial non finite set

( the non empty non trivial non finite set ) is () ()

S is () ()

the of S is set

S is () ()

the of S is set

S is () ()

S is ()

the of S is set

X is trivial finite set

S is ()

S is ()

the of S is set

S is ()

(S) is Element of the of S

the of S is set

the of S is Element of the of S

In ({},2) is epsilon-transitive epsilon-connected ordinal Element of 2

In (1,2) is epsilon-transitive epsilon-connected ordinal Element of 2

(2,(In ({},2)),(In (1,2))) is () ()

S is () ()

(S) is (S) Element of the of S

the of S is set

the of S is Element of the of S

(S) is Element of the of S

the of S is Element of the of S

S is () () () ()

(S) is Element of the of S

the of S is non empty non trivial set

the of S is Element of the of S

(S) is (S) Element of the of S

the of S is Element of the of S

S is ()

the of S is set

(S) is Element of bool the of S

bool the of S is set

({},{}) is () ()

S is () ()

the of S is set

the of S is set

S is () ()

the of S is set

(1,1) is () ()

S is () ()

the of S is set

the of S is set

S is () ()

the of S is set

X is () ()

the of X is non empty set

S is ()

the of S is set

y is Element of the of X

the of S --> y is Relation-like the of S -defined the of X -valued V6() total V18( the of S, the of X) Element of bool [: the of S, the of X:]

[: the of S, the of X:] is set

bool [: the of S, the of X:] is set

S is ()

the of S is set

(S) is (S) Element of the of S

the of S is Element of the of S

In ({},2) is epsilon-transitive epsilon-connected ordinal Element of 2

(2,(In ({},2))) is () ()

S is () () ()

the of S is non empty non trivial set

X is Element of the of S

y is Element of the of S

(S) is (S) Element of the of S

the of S is Element of the of S

(S) is (S) Element of the of S

the of S is Element of the of S

(S) is (S) Element of the of S

the of S is Element of the of S

S is set

X is ()

the of X is set

[:S, the of X:] is set

bool [:S, the of X:] is set

S is ()

the of S is set

card the of S is epsilon-transitive epsilon-connected ordinal cardinal set

S is ()

the of S is set

(S) is non proper Element of bool the of S

bool the of S is set

(S) is (S) Element of the of S

the of S is Element of the of S

{(S)} is non empty trivial finite 1 -element set

(S) \ {(S)} is Element of bool the of S

S is () ()

the of S is non empty set

(S) is Element of bool the of S

bool the of S is set

(S) is non empty non proper Element of bool the of S

(S) is (S) Element of the of S

the of S is Element of the of S

{(S)} is non empty trivial finite 1 -element set

(S) \ {(S)} is Element of bool the of S

X is Element of the of S

S is () ()

the of S is non empty set

(S) is (S) Element of the of S

the of S is Element of the of S

X is Element of the of S

X is Element of the of S

y is Element of the of S

S is () () ()

(S) is Element of bool the of S

the of S is non empty non trivial set

bool the of S is set

(S) is non empty non proper Element of bool the of S

(S) is (S) Element of the of S

the of S is Element of the of S

{(S)} is non empty trivial finite 1 -element set

(S) \ {(S)} is Element of bool the of S

X is Element of the of S

In ({},1) is epsilon-transitive epsilon-connected ordinal Element of 1

(1,(In ({},1))) is () ()

S is () () () ()

(S) is finite Element of bool the of S

the of S is non empty trivial finite 1 -element set

bool the of S is finite V36() set

(S) is non empty non proper finite Element of bool the of S

(S) is (S) Element of the of S

the of S is Element of the of S

{(S)} is non empty trivial finite 1 -element set

(S) \ {(S)} is finite Element of bool the of S

X is Element of the of S

{(S)} is non empty trivial finite 1 -element Element of bool the of S

S is () ()

the of S is non empty set

bool the of S is set

the Element of the of S is Element of the of S

{ the Element of the of S} is non empty trivial finite 1 -element Element of bool the of S

S is () () () ()

(S) is (S) Element of the of S

the of S is non empty non trivial set

the of S is Element of the of S

(S) is non empty Element of bool the of S

bool the of S is set

(S) is non empty non proper Element of bool the of S

(S) is (S) Element of the of S

the of S is Element of the of S

{(S)} is non empty trivial finite 1 -element set

(S) \ {(S)} is Element of bool the of S

{(S)} is non empty trivial finite 1 -element Element of bool the of S

S is () ()

(S) is epsilon-transitive epsilon-connected ordinal cardinal set

the of S is finite set

card the of S is epsilon-transitive epsilon-connected ordinal natural finite cardinal complex set

S is () () ()

(S) is epsilon-transitive epsilon-connected ordinal natural finite cardinal complex set

the of S is non empty finite set

card the of S is non empty epsilon-transitive epsilon-connected ordinal natural finite cardinal complex set

X is epsilon-transitive epsilon-connected ordinal natural finite cardinal complex set

S is () () ()

the of S is non empty non trivial set

bool the of S is set

X is Element of the of S

y is Element of the of S

{X,y} is non empty finite Element of bool the of S

A is Element of bool the of S

S is ()

(S) is (S) Element of the of S

the of S is set

the of S is Element of the of S

(S) is Element of bool the of S

bool the of S is set

(S) is non proper Element of bool the of S

{(S)} is non empty trivial finite 1 -element set

(S) \ {(S)} is Element of bool the of S

S is () ()

the of S is non empty set

(S) is (S) Element of the of S

the of S is Element of the of S

{(S)} is non empty trivial finite 1 -element Element of bool the of S

bool the of S is set

(S) is Element of bool the of S

(S) is non empty non proper Element of bool the of S

{(S)} is non empty trivial finite 1 -element set

(S) \ {(S)} is Element of bool the of S

{(S)} \/ (S) is non empty Element of bool the of S

S is epsilon-transitive epsilon-connected ordinal cardinal set

the S -element set is S -element set

( the S -element set ) is () ()

X is () ()

the of X is set

S is epsilon-transitive epsilon-connected ordinal cardinal set

X is (S) ()

the of X is set

S is ()

the of S is set

S is ()

the of S is set

S is ()

the of S is set

S is ()

the of S is set

S is ()

the of S is set

S is ()

the of S is set

S is ()

the of S is set

the of S is set

S is ()

(1,1) is () ()

S is () ()

the of S is set

S is () ()

the of S is set

(1,{{},1}) is () ()

S is () ()

S is () ()

the of S is set

S is ()

the of S is set

S is ()