:: STIRL2_1 semantic presentation

REAL is V50() V51() V52() V56() V68() V69() V71() set
NAT is epsilon-transitive epsilon-connected ordinal non empty non trivial V50() V51() V52() V53() V54() V55() V56() non finite V66() V68() cardinal limit_cardinal Element of bool REAL
bool REAL is non empty set
RAT is V50() V51() V52() V53() V56() set

COMPLEX is V50() V56() set
INT is V50() V51() V52() V53() V54() V56() set

bool is non empty set

bool is non empty set

bool is non empty set

bool is non empty set

bool is non empty set

bool is non empty set

bool is non empty set
is Relation-like RAT -valued INT -valued non empty non trivial V40() V41() V42() V43() non finite V92() set
is Relation-like RAT -valued INT -valued non empty non trivial V40() V41() V42() V43() non finite V92() set
bool is non empty non trivial non finite set
NAT is epsilon-transitive epsilon-connected ordinal non empty non trivial V50() V51() V52() V53() V54() V55() V56() non finite V66() V68() cardinal limit_cardinal set
bool NAT is non empty non trivial non finite set
bool NAT is non empty non trivial non finite set

bool is non empty set
1 is epsilon-transitive epsilon-connected ordinal natural non empty V33() V34() integer V36() ext-real positive non negative V50() V51() V52() V53() V54() V55() finite V66() V67() V68() V69() V70() cardinal Element of NAT
{{},1} is non empty V50() V51() V52() V53() V54() V55() finite V61() V66() V67() V68() V69() V70() set
2 is epsilon-transitive epsilon-connected ordinal natural non empty V33() V34() integer V36() ext-real positive non negative V50() V51() V52() V53() V54() V55() finite V66() V67() V68() V69() V70() cardinal Element of NAT
3 is epsilon-transitive epsilon-connected ordinal natural non empty V33() V34() integer V36() ext-real positive non negative V50() V51() V52() V53() V54() V55() finite V66() V67() V68() V69() V70() cardinal Element of NAT

is non empty trivial functional V50() V51() V52() V53() V54() V55() finite V61() V66() V67() V68() V69() V70() 1 -element set

2 ! is V33() V34() ext-real Element of REAL
Ne is non empty V50() V51() V52() V53() V54() V55() V66() V68() Element of bool NAT

Ke is ext-real set
Ne is non empty V50() V51() V52() V53() V54() V55() V66() V68() Element of bool NAT

Ke is non empty V50() V51() V52() V53() V54() V55() V66() V68() Element of bool NAT

min ((min Ne),(min Ke)) is epsilon-transitive epsilon-connected ordinal natural V33() V34() integer V36() ext-real non negative V50() V51() V52() V53() V54() V55() finite V68() V69() V70() cardinal Element of NAT
Ne \/ Ke is non empty V50() V51() V52() V53() V54() V55() V66() V68() Element of bool NAT
min (Ne \/ Ke) is epsilon-transitive epsilon-connected ordinal natural V33() V34() integer V36() ext-real non negative V50() V51() V52() V53() V54() V55() finite V68() V69() V70() cardinal Element of NAT
min ((min Ke),(min Ne)) is epsilon-transitive epsilon-connected ordinal natural V33() V34() integer V36() ext-real non negative V50() V51() V52() V53() V54() V55() finite V68() V69() V70() cardinal Element of NAT
Ke \/ Ne is non empty V50() V51() V52() V53() V54() V55() V66() V68() Element of bool NAT
I1 is ext-real set
Ne is V50() V51() V52() V53() V54() V55() V68() Element of bool NAT

Ke is V50() V51() V52() V53() V54() V55() V68() Element of bool NAT

min ((min* Ne),(min* Ke)) is epsilon-transitive epsilon-connected ordinal natural V33() V34() integer V36() ext-real non negative V50() V51() V52() V53() V54() V55() finite V68() V69() V70() cardinal Element of NAT
Ne \/ Ke is V50() V51() V52() V53() V54() V55() V68() Element of bool NAT
min* (Ne \/ Ke) is epsilon-transitive epsilon-connected ordinal natural V33() V34() integer V36() ext-real non negative V50() V51() V52() V53() V54() V55() finite V68() V69() V70() cardinal Element of NAT
I1 is non empty V50() V51() V52() V53() V54() V55() V66() V68() Element of bool NAT

F is non empty V50() V51() V52() V53() V54() V55() V66() V68() Element of bool NAT
F \/ I1 is non empty V50() V51() V52() V53() V54() V55() V66() V68() Element of bool NAT
min (F \/ I1) is epsilon-transitive epsilon-connected ordinal natural V33() V34() integer V36() ext-real non negative V50() V51() V52() V53() V54() V55() finite V68() V69() V70() cardinal Element of NAT

Ne is V50() V51() V52() V53() V54() V55() V68() Element of bool NAT

Ke is V50() V51() V52() V53() V54() V55() V68() Element of bool NAT
Ne /\ Ke is V50() V51() V52() V53() V54() V55() V68() Element of bool NAT
Ne \ Ke is V50() V51() V52() V53() V54() V55() V68() Element of bool NAT
min* (Ne \ Ke) is epsilon-transitive epsilon-connected ordinal natural V33() V34() integer V36() ext-real non negative V50() V51() V52() V53() V54() V55() finite V68() V69() V70() cardinal Element of NAT
Ne is epsilon-transitive epsilon-connected ordinal natural V33() V34() integer V36() ext-real non negative V50() V51() V52() V53() V54() V55() finite V68() V69() V70() cardinal Element of NAT
{Ne} is non empty trivial V50() V51() V52() V53() V54() V55() finite V61() V66() V67() V68() V69() V70() 1 -element Element of bool NAT

Ne is epsilon-transitive epsilon-connected ordinal natural V33() V34() integer V36() ext-real non negative V50() V51() V52() V53() V54() V55() finite V68() V69() V70() cardinal Element of NAT
Ke is epsilon-transitive epsilon-connected ordinal natural V33() V34() integer V36() ext-real non negative V50() V51() V52() V53() V54() V55() finite V68() V69() V70() cardinal Element of NAT
{Ne,Ke} is non empty V50() V51() V52() V53() V54() V55() finite V61() V66() V67() V68() V69() V70() Element of bool NAT
min* {Ne,Ke} is epsilon-transitive epsilon-connected ordinal natural V33() V34() integer V36() ext-real non negative V50() V51() V52() V53() V54() V55() finite V68() V69() V70() cardinal Element of NAT
min (Ne,Ke) is epsilon-transitive epsilon-connected ordinal natural V33() V34() integer V36() ext-real non negative V50() V51() V52() V53() V54() V55() finite V68() V69() V70() cardinal Element of NAT
min {Ne,Ke} is epsilon-transitive epsilon-connected ordinal natural V33() V34() integer V36() ext-real non negative V50() V51() V52() V53() V54() V55() finite V68() V69() V70() cardinal Element of NAT
{Ne} is non empty trivial V50() V51() V52() V53() V54() V55() finite V61() V66() V67() V68() V69() V70() 1 -element Element of bool NAT

{Ke} is non empty trivial V50() V51() V52() V53() V54() V55() finite V61() V66() V67() V68() V69() V70() 1 -element Element of bool NAT
{Ne} \/ {Ke} is non empty V50() V51() V52() V53() V54() V55() finite V61() V66() V67() V68() V69() V70() Element of bool NAT

min ((min {Ne}),(min {Ke})) is epsilon-transitive epsilon-connected ordinal natural V33() V34() integer V36() ext-real non negative V50() V51() V52() V53() V54() V55() finite V68() V69() V70() cardinal Element of NAT
Ne is epsilon-transitive epsilon-connected ordinal natural V33() V34() integer V36() ext-real non negative V50() V51() V52() V53() V54() V55() finite V68() V69() V70() cardinal Element of NAT
Ke is epsilon-transitive epsilon-connected ordinal natural V33() V34() integer V36() ext-real non negative V50() V51() V52() V53() V54() V55() finite V68() V69() V70() cardinal Element of NAT

{Ne,Ke,F} is non empty V50() V51() V52() V53() V54() V55() finite V66() V67() V68() V69() V70() Element of bool NAT
min* {Ne,Ke,F} is epsilon-transitive epsilon-connected ordinal natural V33() V34() integer V36() ext-real non negative V50() V51() V52() V53() V54() V55() finite V68() V69() V70() cardinal Element of NAT
min (Ke,F) is epsilon-transitive epsilon-connected ordinal natural V33() V34() integer V36() ext-real non negative V50() V51() V52() V53() V54() V55() finite V68() V69() V70() cardinal Element of NAT
min (Ne,(min (Ke,F))) is epsilon-transitive epsilon-connected ordinal natural V33() V34() integer V36() ext-real non negative V50() V51() V52() V53() V54() V55() finite V68() V69() V70() cardinal Element of NAT
min {Ne,Ke,F} is epsilon-transitive epsilon-connected ordinal natural V33() V34() integer V36() ext-real non negative V50() V51() V52() V53() V54() V55() finite V68() V69() V70() cardinal Element of NAT
{Ne} is non empty trivial V50() V51() V52() V53() V54() V55() finite V61() V66() V67() V68() V69() V70() 1 -element Element of bool NAT
{Ke,F} is non empty V50() V51() V52() V53() V54() V55() finite V61() V66() V67() V68() V69() V70() Element of bool NAT
{Ne} \/ {Ke,F} is non empty V50() V51() V52() V53() V54() V55() finite V61() V66() V67() V68() V69() V70() Element of bool NAT

min {Ke,F} is epsilon-transitive epsilon-connected ordinal natural V33() V34() integer V36() ext-real non negative V50() V51() V52() V53() V54() V55() finite V68() V69() V70() cardinal Element of NAT
min ((min {Ne}),(min {Ke,F})) is epsilon-transitive epsilon-connected ordinal natural V33() V34() integer V36() ext-real non negative V50() V51() V52() V53() V54() V55() finite V68() V69() V70() cardinal Element of NAT

Ke is set
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural V33() V34() integer V36() ext-real non negative V50() V51() V52() V53() V54() V55() finite V68() V69() V70() cardinal Element of NAT : not Ne <= b1 } is set

Ke is epsilon-transitive epsilon-connected ordinal natural V33() V34() integer V36() ext-real non negative V50() V51() V52() V53() V54() V55() finite V68() V69() V70() cardinal Element of Ne

Ne - 1 is V33() V34() integer V36() ext-real Element of INT
Ke is non empty V50() V51() V52() V53() V54() V55() V66() V68() Element of bool NAT

{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural V33() V34() integer V36() ext-real non negative V50() V51() V52() V53() V54() V55() finite V68() V69() V70() cardinal Element of NAT : not Ne <= b1 } is set

Ke - 1 is V33() V34() integer V36() ext-real Element of INT
{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural V33() V34() integer V36() ext-real non negative V50() V51() V52() V53() V54() V55() finite V68() V69() V70() cardinal Element of NAT : not Ke <= b1 } is set

(Ke - 1) + 1 is V33() V34() integer V36() ext-real Element of INT

{ b1 where b1 is epsilon-transitive epsilon-connected ordinal natural V33() V34() integer V36() ext-real non negative V50() V51() V52() V53() V54() V55() finite V68() V69() V70() cardinal Element of NAT : not Ne <= b1 } is set

Ne - 1 is V33() V34() integer V36() ext-real Element of INT
Ke is non empty V50() V51() V52() V53() V54() V55() V66() V68() Element of bool NAT

Ne - 1 is V33() V34() integer V36() ext-real Element of INT
{(Ne - 1)} is non empty trivial V50() V51() V52() V53() V54() finite V66() V67() V68() V69() V70() 1 -element Element of bool REAL
Ke is non empty V50() V51() V52() V53() V54() V55() V66() V68() Element of bool NAT

F is set
I1 is epsilon-transitive epsilon-connected ordinal natural V33() V34() integer V36() ext-real non negative V50() V51() V52() V53() V54() V55() finite V68() V69() V70() cardinal Element of NAT

Ne - 1 is V33() V34() integer V36() ext-real Element of INT
Ke is V50() V51() V52() V53() V54() V55() V68() Element of bool NAT

Ke is set
[:Ne,Ke:] is Relation-like set
bool [:Ne,Ke:] is non empty set

I1 is set
F " I1 is finite set
I2 is set
F " I1 is V50() V51() V52() V53() V54() V55() finite V68() V69() V70() Element of bool Ne
bool Ne is non empty finite V61() set
Ne is set

[:Ne,Ke:] is Relation-like RAT -valued INT -valued V40() V41() V42() V43() V92() set
bool [:Ne,Ke:] is non empty set
F is Relation-like Ne -defined Ke -valued Function-like quasi_total V40() V41() V42() V43() V92() Element of bool [:Ne,Ke:]
I1 is set

dom F is Element of bool Ne
bool Ne is non empty set
rng F is V50() V51() V52() V53() V54() V55() finite V68() V69() V70() Element of bool Ke
bool Ke is non empty finite V61() set
dom F is Element of bool Ne
bool Ne is non empty set
dom F is Element of bool Ne
bool Ne is non empty set

[:Ne,Ke:] is Relation-like RAT -valued INT -valued V40() V41() V42() V43() finite V92() set
bool [:Ne,Ke:] is non empty finite V61() set

[:Ne,Ke:] is Relation-like RAT -valued INT -valued V40() V41() V42() V43() finite V92() set
bool [:Ne,Ke:] is non empty finite V61() set
F is Relation-like Ne -defined Ke -valued Function-like quasi_total V40() V41() V42() V43() finite V92() Element of bool [:Ne,Ke:]

{I2} is non empty trivial V50() V51() V52() V53() V54() V55() finite V61() V66() V67() V68() V69() V70() 1 -element Element of bool REAL
(Ne,Ke,F,{I2}) is V50() V51() V52() V53() V54() V55() finite V68() V69() V70() Element of bool NAT
min* (Ne,Ke,F,{I2}) is epsilon-transitive epsilon-connected ordinal natural V33() V34() integer V36() ext-real non negative V50() V51() V52() V53() V54() V55() finite V68() V69() V70() cardinal Element of NAT
{I1} is non empty trivial V50() V51() V52() V53() V54() V55() finite V61() V66() V67() V68() V69() V70() 1 -element Element of bool REAL
(Ne,Ke,F,{I1}) is V50() V51() V52() V53() V54() V55() finite V68() V69() V70() Element of bool NAT
min* (Ne,Ke,F,{I1}) is epsilon-transitive epsilon-connected ordinal natural V33() V34() integer V36() ext-real non negative V50() V51() V52() V53() V54() V55() finite V68() V69() V70() cardinal Element of NAT
rng F is V50() V51() V52() V53() V54() V55() finite V68() V69() V70() Element of bool Ke
bool Ke is non empty finite V61() set

[:Ke,Ne:] is Relation-like RAT -valued INT -valued V40() V41() V42() V43() finite V92() set
bool [:Ke,Ne:] is non empty finite V61() set
Ke - 1 is V33() V34() integer V36() ext-real Element of INT

{F} is non empty trivial V50() V51() V52() V53() V54() V55() finite V61() V66() V67() V68() V69() V70() 1 -element Element of bool REAL
I1 is Relation-like Ke -defined Ne -valued Function-like quasi_total V40() V41() V42() V43() finite V92() Element of bool [:Ke,Ne:]
(Ke,Ne,I1,{F}) is V50() V51() V52() V53() V54() V55() finite V68() V69() V70() Element of bool NAT
min* (Ke,Ne,I1,{F}) is epsilon-transitive epsilon-connected ordinal natural V33() V34() integer V36() ext-real non negative V50() V51() V52() V53() V54() V55() finite V68() V69() V70() cardinal Element of NAT
I2 is set
dom I1 is V50() V51() V52() V53() V54() V55() finite V68() V69() V70() Element of bool Ke
bool Ke is non empty finite V61() set

[:Ne,Ke:] is Relation-like RAT -valued INT -valued V40() V41() V42() V43() finite V92() set
bool [:Ne,Ke:] is non empty finite V61() set
F is Relation-like Ne -defined Ke -valued Function-like quasi_total V40() V41() V42() V43() finite V92() Element of bool [:Ne,Ke:]
rng F is V50() V51() V52() V53() V54() V55() finite V68() V69() V70() Element of bool Ke
bool Ke is non empty finite V61() set
dom F is V50() V51() V52() V53() V54() V55() finite V68() V69() V70() Element of bool Ne
bool Ne is non empty finite V61() set

[:Ne,Ke:] is Relation-like RAT -valued INT -valued V40() V41() V42() V43() finite V92() set
bool [:Ne,Ke:] is non empty finite V61() set
F is Relation-like Ne -defined Ke -valued Function-like quasi_total V40() V41() V42() V43() finite V92() Element of bool [:Ne,Ke:]
rng F is V50() V51() V52() V53() V54() V55() finite V68() V69() V70() Element of bool Ke
bool Ke is non empty finite V61() set

{I1} is non empty trivial V50() V51() V52() V53() V54() V55() finite V61() V66() V67() V68() V69() V70() 1 -element Element of bool REAL
(Ne,Ke,F,{I1}) is V50() V51() V52() V53() V54() V55() finite V68() V69() V70() Element of bool NAT
min* (Ne,Ke,F,{I1}) is epsilon-transitive epsilon-connected ordinal natural V33() V34() integer V36() ext-real non negative V50() V51() V52() V53() V54() V55() finite V68() V69() V70() cardinal Element of NAT
I1 + 1 is epsilon-transitive epsilon-connected ordinal natural non empty V33() V34() integer V36() ext-real positive non negative V50() V51() V52() V53() V54() V55() finite V66() V67() V68() V69() V70() cardinal Element of NAT
{(I1 + 1)} is non empty trivial V50() V51() V52() V53() V54() V55() finite V61() V66() V67() V68() V69() V70() 1 -element Element of bool REAL
(Ne,Ke,F,{(I1 + 1)}) is V50() V51() V52() V53() V54() V55() finite V68() V69() V70() Element of bool NAT
min* (Ne,Ke,F,{(I1 + 1)}) is epsilon-transitive epsilon-connected ordinal natural V33() V34() integer V36() ext-real non negative V50() V51() V52() V53() V54() V55() finite V68() V69() V70() cardinal Element of NAT
{(I1 + 1)} is non empty trivial V50() V51() V52() V53() V54() V55() finite V61() V66() V67() V68() V69() V70() 1 -element Element of bool NAT
(Ne,Ke,F,{(I1 + 1)}) is V50() V51() V52() V53() V54() V55() finite V68() V69() V70() Element of bool NAT
min* (Ne,Ke,F,{(I1 + 1)}) is epsilon-transitive epsilon-connected ordinal natural V33() V34() integer V36() ext-real non negative V50() V51() V52() V53() V54() V55() finite V68() V69() V70() cardinal Element of NAT
is non empty trivial functional V50() V51() V52() V53() V54() V55() finite V61() V66() V67() V68() V69() V70() 1 -element Element of bool REAL
(Ne,Ke,F,) is V50() V51() V52() V53() V54() V55() finite V68() V69() V70() Element of bool NAT
min* (Ne,Ke,F,) is epsilon-transitive epsilon-connected ordinal natural V33() V34() integer V36() ext-real non negative V50() V51() V52() V53() V54() V55() finite V68() V69() V70() cardinal Element of NAT

{I1} is non empty trivial V50() V51() V52() V53() V54() V55() finite V61() V66() V67() V68() V69() V70() 1 -element Element of bool REAL
(Ne,Ke,F,{I1}) is V50() V51() V52() V53() V54() V55() finite V68() V69() V70() Element of bool NAT
min* (Ne,Ke,F,{I1}) is epsilon-transitive epsilon-connected ordinal natural V33() V34() integer V36() ext-real non negative V50() V51() V52() V53() V54() V55() finite V68() V69() V70() cardinal Element of NAT

[:Ke,Ne:] is Relation-like RAT -valued INT -valued V40() V41() V42() V43() finite V92() set
bool [:Ke,Ne:] is non empty finite V61() set
Ke - Ne is V33() V34() integer V36() ext-real Element of INT
F is Relation-like Ke -defined Ne -valued Function-like quasi_total V40() V41() V42() V43() finite V92() Element of bool [:Ke,Ne:]

{I1} is non empty trivial V50() V51() V52() V53() V54() V55() finite V61() V66() V67() V68() V69() V70() 1 -element Element of bool REAL
(Ke,Ne,F,{I1}) is V50() V51() V52() V53() V54() V55() finite V68() V69() V70() Element of bool NAT
min* (Ke,Ne,F,{I1}) is epsilon-transitive epsilon-connected ordinal natural V33() V34() integer V36() ext-real non negative V50() V51() V52() V53() V54() V55() finite V68() V69() V70() cardinal Element of NAT
(Ke - Ne) + I1 is V33() V34() integer V36() ext-real Element of INT
Ne - 1 is V33() V34() integer V36() ext-real Element of INT
I1 is epsilon-transitive epsilon-connected ordinal natural V33() V34() integer V36() ext-real non negative V50() V51() V52() V53() V54() V55() finite V68() V69() V70() cardinal Element of NAT
I1 + 1 is epsilon-transitive epsilon-connected ordinal natural non empty V33() V34() integer V36() ext-real positive non negative V50() V51() V52() V53() V54() V55() finite V66() V67() V68() V69() V70() cardinal Element of NAT
rng F is V50() V51() V52() V53() V54() V55() finite V68() V69() V70() Element of bool Ne
bool Ne is non empty finite V61() set
P1 is V33() V34() integer ext-real set
{P1} is non empty trivial V50() V51() V52() V53() V54() finite V66() V67() V68() V69() V70() 1 -element Element of bool REAL
(Ke,Ne,F,{P1}) is V50() V51() V52() V53() V54() V55() finite V68() V69() V70() Element of bool NAT
min* (Ke,Ne,F,{P1}) is epsilon-transitive epsilon-connected ordinal natural V33() V34() integer V36() ext-real non negative V50() V51() V52() V53() V54() V55() finite V68() V69() V70() cardinal Element of NAT
(Ke - Ne) + P1 is V33() V34() integer V36() ext-real Element of INT
P1 - 1 is V33() V34() integer V36() ext-real Element of INT
{(P1 - 1)} is non empty trivial V50() V51() V52() V53() V54() finite V66() V67() V68() V69() V70() 1 -element Element of bool REAL
(Ke,Ne,F,{(P1 - 1)}) is V50() V51() V52() V53() V54() V55() finite V68() V69() V70() Element of bool NAT
min* (Ke,Ne,F,{(P1 - 1)}) is epsilon-transitive epsilon-connected ordinal natural V33() V34() integer V36() ext-real non negative V50() V51() V52() V53() V54() V55() finite V68() V69() V70() cardinal Element of NAT
(Ke - Ne) + (P1 - 1) is V33() V34() integer V36() ext-real Element of INT
P2 is epsilon-transitive epsilon-connected ordinal natural V33() V34() integer V36() ext-real non negative V50() V51() V52() V53() V54() V55() finite V68() V69() V70() cardinal Element of NAT
P2 + 1 is epsilon-transitive epsilon-connected ordinal natural non empty V33() V34() integer V36() ext-real positive non negative V50() V51() V52() V53() V54() V55() finite V66() V67() V68() V69() V70() cardinal Element of NAT
{(P2 + 1)} is non empty trivial V50() V51() V52() V53() V54() V55() finite V61() V66() V67() V68() V69() V70() 1 -element Element of bool NAT
(Ke,Ne,F,{(P2 + 1)}) is V50() V51() V52() V53() V54() V55() finite V68() V69() V70() Element of bool NAT
min* (Ke,Ne,F,{(P2 + 1)}) is epsilon-transitive epsilon-connected ordinal natural V33() V34() integer V36() ext-real non negative V50() V51() V52() V53() V54() V55() finite V68() V69() V70() cardinal Element of NAT
{P2} is non empty trivial V50() V51() V52() V53() V54() V55() finite V61() V66() V67() V68() V69() V70() 1 -element Element of bool NAT
(Ke,Ne,F,{P2}) is V50() V51() V52() V53() V54() V55() finite V68() V69() V70() Element of bool NAT
min* (Ke,Ne,F,{P2}) is epsilon-transitive epsilon-connected ordinal natural V33() V34() integer V36() ext-real non negative V50() V51() V52() V53() V54() V55() finite V68() V69() V70() cardinal Element of NAT
I2 is epsilon-transitive epsilon-connected ordinal natural V33() V34() integer V36() ext-real non negative V50() V51() V52() V53() V54() V55() finite V68() V69() V70() cardinal Element of NAT
I2 + P2 is epsilon-transitive epsilon-connected ordinal natural V33() V34() integer V36() ext-real non negative V50() V51() V52() V53() V54() V55() finite V68() V69() V70() cardinal Element of NAT
(I2 + P2) + 1 is epsilon-transitive epsilon-connected ordinal natural non empty V33() V34() integer V36() ext-real positive non negative V50() V51() V52() V53() V54() V55() finite V66() V67() V68() V69() V70() cardinal Element of NAT
{I1} is non empty trivial V50() V51() V52() V53() V54() V55() finite V61() V66() V67() V68() V69() V70() 1 -element Element of bool REAL
(Ke,Ne,F,{I1}) is V50() V51() V52() V53() V54() V55() finite V68() V69() V70() Element of bool NAT
min* (Ke,Ne,F,{I1}) is epsilon-transitive epsilon-connected ordinal natural V33() V34() integer V36() ext-real non negative V50() V51() V52() V53() V54() V55() finite V68() V69() V70() cardinal Element of NAT
(Ke - Ne) + I1 is V33() V34() integer V36() ext-real Element of INT
{I1} is non empty trivial V50() V51() V52() V53() V54() V55() finite V61() V66() V67() V68() V69() V70() 1 -element Element of bool NAT
(Ke,Ne,F,{I1}) is V50() V51() V52() V53() V54() V55() finite V68() V69() V70() Element of bool NAT
min* (Ke,Ne,F,{I1}) is epsilon-transitive epsilon-connected ordinal natural V33() V34() integer V36() ext-real non negative V50() V51() V52() V53() V54() V55() finite V68() V69() V70() cardinal Element of NAT
Ke - 1 is V33() V34() integer V36() ext-real Element of INT

{I2} is non empty trivial V50() V51() V52() V53() V54() V55() finite V61() V66() V67() V68() V69() V70() 1 -element Element of bool REAL
(Ke,Ne,F,{I2}) is V50() V51() V52() V53() V54() V55() finite V68() V69() V70() Element of bool NAT
min* (Ke,Ne,F,{I2}) is epsilon-transitive epsilon-connected ordinal natural V33() V34() integer V36() ext-real non negative V50() V51() V52() V53() V54() V55() finite V68() V69() V70() cardinal Element of NAT
(Ke - Ne) + I2 is V33() V34() integer V36() ext-real Element of INT

{I2} is non empty trivial V50() V51() V52() V53() V54() V55() finite V61() V66() V67() V68() V69() V70() 1 -element Element of bool REAL
(Ke,Ne,F,{I2}) is V50() V51() V52() V53() V54() V55() finite V68() V69() V70() Element of bool NAT
min* (Ke,Ne,F,{I2}) is epsilon-transitive epsilon-connected ordinal natural V33() V34() integer V36() ext-real non negative V50() V51() V52() V53() V54() V55() finite V68() V69() V70() cardinal Element of NAT
(Ke - Ne) + I2 is V33() V34() integer V36() ext-real Element of INT

{I1} is non empty trivial V50() V51() V52() V53() V54() V55() finite V61() V66() V67() V68() V69() V70() 1 -element Element of bool REAL
(Ke,Ne,F,{I1}) is V50() V51() V52() V53() V54() V55() finite V68() V69() V70() Element of bool NAT
min* (Ke,Ne,F,{I1}) is epsilon-transitive epsilon-connected ordinal natural V33() V34() integer V36() ext-real non negative V50() V51() V52() V53() V54() V55() finite V68() V69() V70() cardinal Element of NAT
(Ke - Ne) + I1 is V33() V34() integer V36() ext-real Element of INT

id Ne is Relation-like Ne -defined Ne -valued RAT -valued INT -valued Function-like one-to-one V24(Ne) quasi_total V40() V41() V42() V43() V44() V46() finite V92() Element of bool [:Ne,Ne:]
[:Ne,Ne:] is Relation-like RAT -valued INT -valued V40() V41() V42() V43() finite V92() set
bool [:Ne,Ne:] is non empty finite V61() set

[:Ne,Ke:] is Relation-like RAT -valued INT -valued V40() V41() V42() V43() finite V92() set
bool [:Ne,Ke:] is non empty finite V61() set
F is Relation-like Ne -defined Ke -valued Function-like quasi_total V40() V41() V42() V43() finite V92() Element of bool [:Ne,Ke:]
I1 is set
(Ne,Ke,F,I1) is epsilon-transitive epsilon-connected ordinal natural V33() V34() integer V36() ext-real non negative V50() V51() V52() V53() V54() V55() finite V68() V69() V70() cardinal Element of Ke
dom F is V50() V51() V52() V53() V54() V55() finite V68() V69() V70() Element of bool Ne
bool Ne is non empty finite V61() set
I1 is set
I2 is epsilon-transitive epsilon-connected ordinal natural V33() V34() integer V36() ext-real non negative V50() V51() V52() V53() V54() V55() finite V68() V69() V70() cardinal Element of NAT
rng F is V50() V51() V52() V53() V54() V55() finite V68() V69() V70() Element of bool Ke
bool Ke is non empty finite V61() set
dom F is V50() V51() V52() V53() V54() V55() finite V68() V69() V70() Element of bool Ne
bool Ne is non empty finite V61() set
{I2} is non empty trivial V50() V51() V52() V53() V54() V55() finite V61() V66() V67() V68() V69() V70() 1 -element Element of bool NAT
(Ne,Ke,F,{I2}) is V50() V51() V52() V53() V54() V55() finite V68() V69() V70() Element of bool NAT
P2 is set
(Ne,Ke,F,P2) is epsilon-transitive epsilon-connected ordinal natural V33() V34() integer V36() ext-real non negative V50() V51() V52() V53() V54() V55() finite V68() V69() V70() cardinal Element of Ke
min* (Ne,Ke,F,{I2}) is epsilon-transitive epsilon-connected ordinal natural V33() V34() integer V36() ext-real non negative V50() V51() V52() V53() V54() V55() finite V68() V69() V70() cardinal Element of NAT
Ne - Ke is V33() V34() integer V36() ext-real Element of INT
(Ne - Ke) + I2 is V33() V34() integer V36() ext-real Element of INT
P1 is non empty V50() V51() V52() V53() V54() V55() V66() V68() Element of bool NAT

(Ne,Ke,F,I2) is epsilon-transitive epsilon-connected ordinal natural V33() V34() integer V36() ext-real non negative V50() V51() V52() V53() V54() V55() finite V68() V69() V70() cardinal Element of Ke
(Ne,Ke,F,I1) is epsilon-transitive epsilon-connected ordinal natural V33() V34() integer V36() ext-real non negative V50() V51() V52() V53() V54() V55() finite V68() V69() V70() cardinal Element of Ke

[:Ke,Ne:] is Relation-like RAT -valued INT -valued V40() V41() V42() V43() finite V92() set
bool [:Ke,Ne:] is non empty finite V61() set
id Ke is Relation-like Ke -defined Ke -valued RAT -valued INT -valued Function-like one-to-one V24(Ke) quasi_total V40() V41() V42() V43() V44() V46() finite V92() Element of bool [:Ke,Ke:]
[:Ke,Ke:] is Relation-like RAT -valued INT -valued V40() V41() V42() V43() finite V92() set
bool [:Ke,Ke:] is non empty finite V61() set
F is Relation-like Ke -defined Ne -valued Function-like quasi_total V40() V41() V42() V43() finite V92() Element of bool [:Ke,Ne:]

rng F is V50() V51() V52() V53() V54() V55() finite V68() V69() V70() Element of bool Ne
bool Ne is non empty finite V61() set

{I1} is non empty trivial V50() V51() V52() V53() V54() V55() finite V61() V66() V67() V68() V69() V70() 1 -element Element of bool REAL
(Ke,Ne,F,{I1}) is V50() V51() V52() V53() V54() V55() finite V68() V69() V70() Element of bool NAT
dom F is V50() V51() V52() V53() V54() V55() finite V68() V69() V70() Element of bool Ke
bool Ke is non empty finite V61() set
P1 is set
(Ke,Ne,F,P1) is epsilon-transitive epsilon-connected ordinal natural V33() V34() integer V36() ext-real non negative V50() V51() V52() V53() V54() V55() finite V68() V69() V70() cardinal Element of Ne
P2 is set
{P2} is non empty trivial finite 1 -element set
min* (Ke,Ne,F,{I1}) is epsilon-transitive epsilon-connected ordinal natural V33() V34() integer V36() ext-real non negative V50() V51() V52() V53() V54() V55() finite V68() V69() V70() cardinal Element of NAT
{I2} is non empty trivial V50() V51() V52() V53() V54() V55() finite V61() V66() V67() V68() V69() V70() 1 -element Element of bool REAL
(Ke,Ne,F,{I2}) is V50() V51() V52() V53() V54() V55() finite V68() V69() V70() Element of bool NAT
P2 is set
(Ke,Ne,F,P2) is epsilon-transitive epsilon-connected ordinal natural V33() V34() integer V36() ext-real non negative V50() V51() V52() V53() V54() V55() finite V68() V69() V70() cardinal Element of Ne
F is set
{F} is non empty trivial finite 1 -element set
min* (Ke,Ne,F,{I2}) is epsilon-transitive epsilon-connected ordinal natural V33() V34() integer V36() ext-real non negative V50() V51() V52() V53() V54() V55() finite V68() V69() V70() cardinal Element of NAT
I1 is set

[:Ne,Ke:] is Relation-like RAT -valued INT -valued V40() V41() V42() V43() finite V92() set
bool [:Ne,Ke:] is non empty finite V61() set

bool RAT is non empty set
I1 is Relation-like Ne -defined Ke -valued Function-like quasi_total V40() V41() V42() V43() finite V92() Element of bool [:Ne,Ke:]
is non empty trivial functional V50() V51() V52() V53() V54() V55() finite V61() V66() V67() V68() V69() V70() 1 -element Element of bool NAT

dom F is set
rng F is set

bool [:Ne,:] is non empty finite V61() set
I1 is Relation-like Ne -defined -valued Function-like V24(Ne) quasi_total V40() V41() V42() V43() finite V92() Element of bool [:Ne,:]
rng I1 is trivial functional V50() V51() V52() V53() V54() V55() finite V61() V68() V69() V70() Element of bool
bool is non empty finite V61() set
I2 is set
I2 is Relation-like Ne -defined Ke -valued Function-like quasi_total V40() V41() V42() V43() finite V92() Element of bool [:Ne,Ke:]
rng I2 is V50() V51() V52() V53() V54() V55() finite V68() V69() V70() Element of bool Ke
bool Ke is non empty finite V61() set

{P2} is non empty trivial V50() V51() V52() V53() V54() V55() finite V61() V66() V67() V68() V69() V70() 1 -element Element of bool REAL
(Ne,Ke,I2,{P2}) is V50() V51() V52() V53() V54() V55() finite V68() V69() V70() Element of bool NAT
min* (Ne,Ke,I2,{P2}) is epsilon-transitive epsilon-connected ordinal natural V33() V34() integer V36() ext-real non negative V50() V51() V52() V53() V54() V55() finite V68() V69() V70() cardinal Element of NAT
{P1} is non empty trivial V50() V51() V52() V53() V54() V55() finite V61() V66() V67() V68() V69() V70() 1 -element Element of bool REAL
(Ne,Ke,I2,{P1}) is V50() V51() V52() V53() V54() V55() finite V68() V69() V70() Element of bool NAT
min* (Ne,Ke,I2,{P1}) is epsilon-transitive epsilon-connected ordinal natural V33() V34() integer V36() ext-real non negative V50() V51() V52() V53() V54() V55() finite V68() V69() V70() cardinal Element of NAT
F is Relation-like Ne -defined Ke -valued Function-like quasi_total V40() V41() V42() V43() finite V92() Element of bool [:Ne,Ke:]

[:Ne,Ke:] is Relation-like RAT -valued INT -valued V40() V41() V42() V43() finite V92() set
bool [:Ne,Ke:] is non empty finite V61() set

bool RAT is non empty set
I1 is Relation-like Ne -defined Ke -valued Function-like quasi_total V40() V41() V42() V43() finite V92() Element of bool [:Ne,Ke:]
Ke - 1 is V33() V34() integer V36() ext-real Element of INT
I2 is epsilon-transitive epsilon-connected ordinal natural non empty V33() V34() integer V36() ext-real positive non negative V50() V51() V52() V53() V54() V55() finite V66() V67() V68() V69() V70() cardinal Element of NAT
I1 is epsilon-transitive epsilon-connected ordinal natural non empty V33() V34() integer V36() ext-real positive non negative V50() V51() V52() V53() V54() V55() finite V66() V67() V68() V69() V70() cardinal Element of NAT

P1 is epsilon-transitive epsilon-connected ordinal natural V33() V34() integer V36() ext-real non negative V50() V51() V52() V53() V54() V55() finite V68() V69() V70() cardinal Element of I2
min (P1,F) is epsilon-transitive epsilon-connected ordinal natural V33() V34() integer ext-real non negative V50() V51() V52() V53() V54() V55() finite V68() V69() V70() cardinal set
F + 1 is epsilon-transitive epsilon-connected ordinal natural non empty V33() V34() integer V36() ext-real positive non negative V50() V51() V52() V53() V54() V55() finite V66() V67() V68() V69() V70() cardinal Element of NAT
[:I2,I1:] is Relation-like RAT -valued INT -valued non empty V40() V41() V42() V43() finite V92() set
bool [:I2,I1:] is non empty finite V61() set
P1 is Relation-like I2 -defined I1 -valued non empty Function-like V24(I2) quasi_total V40() V41() V42() V43() finite V92() Element of bool [:I2,I1:]
P2 is set
F + 1 is epsilon-transitive epsilon-connected ordinal natural non empty V33() V34() integer V36() ext-real positive non negative V50() V51() V52() V53() V54() V55() finite V66() V67() V68() V69() V70() cardinal Element of NAT

dom P1 is non empty V50() V51() V52() V53() V54() V55() finite V66() V67() V68() V69() V70() Element of bool I2
bool I2 is non empty finite V61() set
min (F,F) is epsilon-transitive epsilon-connected ordinal natural V33() V34() integer V36() ext-real non negative V50() V51() V52() V53() V54() V55() finite V68() V69() V70() cardinal Element of NAT
(I2,I1,P1,F) is epsilon-transitive epsilon-connected ordinal natural V33() V34() integer V36() ext-real non negative V50() V51() V52() V53() V54() V55() finite V68() V69() V70() cardinal Element of I1
rng P1 is non empty V50() V51() V52() V53() V54() V55() finite V66() V67() V68() V69() V70() Element of bool I1
bool I1 is non empty finite V61() set

{P2} is non empty trivial V50() V51() V52() V53() V54() V55() finite V61() V66() V67() V68() V69() V70() 1 -element Element of bool REAL
(I2,I1,P1,{P2}) is V50() V51() V52() V53() V54() V55() finite V68() V69() V70() Element of bool NAT
min* (I2,I1,P1,{P2}) is epsilon-transitive epsilon-connected ordinal natural V33() V34() integer V36() ext-real non negative V50() V51() V52() V53() V54() V55() finite V68() V69() V70() cardinal Element of NAT
min (P2,F) is epsilon-transitive epsilon-connected ordinal natural V33() V34() integer ext-real non negative V50() V51() V52() V53() V54() V55() finite V68() V69() V70() cardinal set
(I2,I1,P1,P2) is epsilon-transitive epsilon-connected ordinal natural V33() V34() integer V36() ext-real non negative V50() V51() V52() V53() V54() V55() finite V68() V69() V70() cardinal Element of I1
F is set
domF is epsilon-transitive epsilon-connected ordinal natural V33() V34() integer V36() ext-real non negative V50() V51() V52() V53() V54() V55() finite V68() V69() V70() cardinal Element of NAT
(I2,I1,P1,domF) is epsilon-transitive epsilon-connected ordinal natural V33() V34() integer V36() ext-real non negative V50() V51() V52() V53() V54() V55() finite V68() V69() V70() cardinal Element of I1
min (domF,F) is epsilon-transitive epsilon-connected ordinal natural V33() V34() integer V36() ext-real non negative V50() V51() V52() V53() V54() V55() finite V68() V69() V70() cardinal Element of NAT

(I2,I1,P1,F) is epsilon-transitive epsilon-connected ordinal natural V33() V34() integer V36() ext-real non negative V50() V51() V52() V53() V54() V55() finite V68() V69() V70() cardinal Element of I1
min (F,P2) is epsilon-transitive epsilon-connected ordinal natural V33() V34() integer ext-real non negative V50() V51() V52() V53() V54() V55() finite V68() V69() V70() cardinal set

{P2} is non empty trivial V50() V51() V52() V53() V54() V55() finite V61() V66() V67() V68() V69() V70() 1 -element Element of bool REAL
(I2,I1,P1,{P2}) is V50() V51() V52() V53() V54() V55() finite V68() V69() V70() Element of bool NAT
min* (I2,I1,P1,{P2}) is epsilon-transitive epsilon-connected ordinal natural V33() V34() integer V36() ext-real non negative V50() V51() V52() V53() V54() V55() finite V68() V69() V70() cardinal Element of NAT
{F} is non empty trivial V50() V51() V52() V53() V54() V55() finite V61() V66() V67() V68() V69() V70() 1 -element Element of bool REAL
(I2,I1,P1,{F}) is V50() V51() V52() V53() V54() V55() finite V68() V69() V70() Element of bool NAT
min* (I2,I1,P1,{F}) is epsilon-transitive epsilon-connected ordinal natural V33() V34() integer V36() ext-real non negative V50() V51() V52() V53() V54() V55() finite V68() V69() V70() cardinal Element of NAT
F is Relation-like Ne -defined Ke -valued Function-like quasi_total V40() V41() V42() V43() finite V92() Element of bool [:Ne,Ke:]
F1() is epsilon-transitive epsilon-connected ordinal natural V33() V34() integer ext-real non negative V50() V51() V52() V53() V54() V55() finite V68() V69() V70() cardinal set
F2() is epsilon-transitive epsilon-connected ordinal natural V33() V34() integer ext-real non negative V50() V51() V52() V53() V54() V55() finite V68() V69() V70() cardinal set
[:F1(),F2():] is Relation-like RAT -valued INT -valued V40() V41() V42() V43() finite V92() set
bool [:F1(),F2():] is non empty finite V61() set
{ b1 where b1 is Relation-like F1() -defined F2() -valued Function-like quasi_total V40() V41() V42() V43() finite V92() Element of bool [:F1(),F2():] : P1[b1] } is set
is non empty trivial functional V50() V51() V52() V53() V54() V55() finite V61() V66() V67() V68() V69() V70() 1 -element Element of bool REAL
Ke is set
F is Relation-like F1() -defined F2() -valued Function-like quasi_total V40() V41() V42() V43() finite V92() Element of bool [:F1(),F2():]
Funcs (F1(),F2()) is functional set
Ke is set
F is Relation-like F1() -defined F2() -valued Function-like quasi_total V40() V41() V42() V43() finite V92() Element of bool [:F1(),F2():]

[:Ne,Ke:] is Relation-like RAT -valued INT -valued V40() V41() V42() V43() finite V92() set
bool [:Ne,Ke:] is non empty finite V61() set
{ b1 where b1 is Relation-like Ne -defined Ke -valued Function-like quasi_total V40() V41() V42() V43() finite V92() Element of bool [:Ne,Ke:] : ( b1 is onto & b1 is (Ne,Ke) ) } is set
{ b1 where b1 is Relation-like Ne -defined Ke -valued Function-like quasi_total V40() V41() V42() V43() finite V92() Element of bool [:Ne,Ke:] : S1[b1] } is set

[:Ne,Ke:] is Relation-like RAT -valued INT -valued V40() V41() V42() V43() finite V92() set
bool [:Ne,Ke:] is non empty finite V61() set
{ b1 where b1 is Relation-like Ne -defined Ke -valued Function-like quasi_total V40() V41() V42() V43() finite V92() Element of bool [:Ne,Ke:] : ( b1 is onto & b1 is (Ne,Ke) ) } is set
card { b1 where b1 is Relation-like Ne -defined Ke -valued Function-like quasi_total V40() V41() V42() V43() finite V92() Element of bool [:Ne,Ke:] : ( b1 is onto & b1 is (Ne,Ke) ) } is epsilon-transitive epsilon-connected ordinal cardinal set

[:Ne,Ke:] is Relation-like RAT -valued INT -valued V40() V41() V42() V43() finite V92() set
bool [:Ne,Ke:] is non empty finite V61() set
{ b1 where b1 is Relation-like Ne -defined Ke -valued Function-like quasi_total V40() V41() V42() V43() finite V92() Element of bool [:Ne,Ke:] : ( b1 is onto & b1 is (Ne,Ke) ) } is set
card { b1 where b1 is Relation-like Ne -defined Ke -valued Function-like quasi_total V40() V41() V42() V43() finite V92() Element of bool [:Ne,Ke:] : ( b1 is onto & b1 is (Ne,Ke) ) } is epsilon-transitive epsilon-connected ordinal cardinal set

(Ne,<