:: HEYTING3 semantic presentation

begin

scheme :: HEYTING3:sch 1
SSubsetUniq{ F1() -> ( ( ) ( ) 1-sorted ) , P1[ ( ( ) ( ) set ) ] } :
for A1, A2 being ( ( ) ( ) Subset of ) st ( for x being ( ( ) ( ) set ) holds
( x : ( ( ) ( ) set ) in A1 : ( ( ) ( ) Subset of ) iff P1[x : ( ( ) ( ) set ) ] ) ) & ( for x being ( ( ) ( ) set ) holds
( x : ( ( ) ( ) set ) in A2 : ( ( ) ( ) Subset of ) iff P1[x : ( ( ) ( ) set ) ] ) ) holds
A1 : ( ( ) ( ) Subset of ) = A2 : ( ( ) ( ) Subset of )
proof end;

registration
let A, x be ( ( ) ( ) set ) ;
cluster [:A : ( ( ) ( ) set ) ,{x : ( ( ) ( ) set ) } : ( ( ) ( non empty finite ) set ) :] : ( ( ) ( Relation-like ) set ) -> Function-like ;
end;

theorem :: HEYTING3:1
for X being ( ( non empty finite ) ( non empty finite V143() V144() V145() V146() V147() V148() V154() V155() V156() V157() V158() ) Subset of ( ( ) ( non empty V107() cup-closed diff-closed preBoolean ) set ) ) ex n being ( ( ) ( V35() V36() V37() V41() V42() V43() V128() V129() ext-real non negative V143() V144() V145() V146() V147() V148() V156() ) Element of NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) st X : ( ( non empty finite ) ( non empty finite V143() V144() V145() V146() V147() V148() V154() V155() V156() V157() V158() ) Subset of ( ( ) ( non empty V107() cup-closed diff-closed preBoolean ) set ) ) c= (Seg n : ( ( ) ( V35() V36() V37() V41() V42() V43() V128() V129() ext-real non negative V143() V144() V145() V146() V147() V148() V156() ) Element of NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) ) : ( ( ) ( finite V51(b2 : ( ( ) ( V35() V36() V37() V41() V42() V43() V128() V129() ext-real non negative V143() V144() V145() V146() V147() V148() V156() ) Element of NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) ) V143() V144() V145() V146() V147() V148() V156() V157() V158() ) Element of bool NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) : ( ( ) ( non empty V107() cup-closed diff-closed preBoolean ) set ) ) \/ {0 : ( ( ) ( Relation-like non-empty empty-yielding functional empty V35() V36() V37() V39() V40() V41() V42() V43() finite finite-yielding V48() FinSequence-like FinSequence-membered V128() V129() ext-real non positive non negative V143() V144() V145() V146() V147() V148() V149() V156() V157() V158() V159() ) Element of NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) } : ( ( ) ( non empty finite V48() V143() V144() V145() V146() V147() V148() V154() V155() V156() V157() V158() ) Element of bool NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) : ( ( ) ( non empty V107() cup-closed diff-closed preBoolean ) set ) ) : ( ( ) ( non empty finite V143() V144() V145() V146() V147() V148() V154() V155() V156() V157() V158() ) Element of bool NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) : ( ( ) ( non empty V107() cup-closed diff-closed preBoolean ) set ) ) ;

theorem :: HEYTING3:2
for X being ( ( finite ) ( finite V143() V144() V145() V146() V147() V148() V156() V157() V158() ) Subset of ( ( ) ( non empty V107() cup-closed diff-closed preBoolean ) set ) ) holds
not for k being ( ( odd ) ( non empty V35() V36() V37() V41() V42() V43() odd V128() V129() ext-real positive non negative V143() V144() V145() V146() V147() V148() V154() V156() ) Element of NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) holds k : ( ( odd ) ( non empty V35() V36() V37() V41() V42() V43() odd V128() V129() ext-real positive non negative V143() V144() V145() V146() V147() V148() V154() V156() ) Element of NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) in X : ( ( finite ) ( finite V143() V144() V145() V146() V147() V148() V156() V157() V158() ) Subset of ( ( ) ( non empty V107() cup-closed diff-closed preBoolean ) set ) ) ;

theorem :: HEYTING3:3
for k being ( ( ) ( V35() V36() V37() V41() V42() V43() V128() V129() ext-real non negative V143() V144() V145() V146() V147() V148() V156() ) Element of NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) )
for X being ( ( non empty finite ) ( Relation-like REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) -defined NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) -valued non empty finite ) Subset of ( ( ) ( non empty V107() cup-closed diff-closed preBoolean ) set ) ) ex n being ( ( non empty ) ( non empty V35() V36() V37() V41() V42() V43() V128() V129() ext-real positive non negative V143() V144() V145() V146() V147() V148() V154() V156() ) Element of NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) st X : ( ( non empty finite ) ( Relation-like REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) -defined NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) -valued non empty finite ) Subset of ( ( ) ( non empty V107() cup-closed diff-closed preBoolean ) set ) ) c= [:((Seg n : ( ( non empty ) ( non empty V35() V36() V37() V41() V42() V43() V128() V129() ext-real positive non negative V143() V144() V145() V146() V147() V148() V154() V156() ) Element of NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) ) : ( ( ) ( non empty finite V51(b3 : ( ( non empty ) ( non empty V35() V36() V37() V41() V42() V43() V128() V129() ext-real positive non negative V143() V144() V145() V146() V147() V148() V154() V156() ) Element of NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) ) V143() V144() V145() V146() V147() V148() V154() V155() V156() V157() V158() ) Element of bool NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) : ( ( ) ( non empty V107() cup-closed diff-closed preBoolean ) set ) ) \/ {0 : ( ( ) ( Relation-like non-empty empty-yielding functional empty V35() V36() V37() V39() V40() V41() V42() V43() finite finite-yielding V48() FinSequence-like FinSequence-membered V128() V129() ext-real non positive non negative V143() V144() V145() V146() V147() V148() V149() V156() V157() V158() V159() ) Element of NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) } : ( ( ) ( non empty finite V48() V143() V144() V145() V146() V147() V148() V154() V155() V156() V157() V158() ) Element of bool NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) : ( ( ) ( non empty V107() cup-closed diff-closed preBoolean ) set ) ) ) : ( ( ) ( non empty finite V143() V144() V145() V146() V147() V148() V154() V155() V156() V157() V158() ) Element of bool NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) : ( ( ) ( non empty V107() cup-closed diff-closed preBoolean ) set ) ) ,{k : ( ( ) ( V35() V36() V37() V41() V42() V43() V128() V129() ext-real non negative V143() V144() V145() V146() V147() V148() V156() ) Element of NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) } : ( ( ) ( non empty finite V143() V144() V145() V146() V147() V148() V154() V155() V156() V157() V158() ) Element of bool NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) : ( ( ) ( non empty V107() cup-closed diff-closed preBoolean ) set ) ) :] : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) -defined NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) -valued Function-like non empty finite ) Element of bool [:NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ,NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) :] : ( ( ) ( Relation-like non empty ) set ) : ( ( ) ( non empty V107() cup-closed diff-closed preBoolean ) set ) ) ;

theorem :: HEYTING3:4
for m being ( ( ) ( V35() V36() V37() V41() V42() V43() V128() V129() ext-real non negative V143() V144() V145() V146() V147() V148() V156() ) Element of NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) )
for X being ( ( non empty finite ) ( Relation-like REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) -defined NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) -valued non empty finite ) Subset of ( ( ) ( non empty V107() cup-closed diff-closed preBoolean ) set ) ) holds
not for k being ( ( non empty ) ( non empty V35() V36() V37() V41() V42() V43() V128() V129() ext-real positive non negative V143() V144() V145() V146() V147() V148() V154() V156() ) Element of NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) holds [((2 : ( ( ) ( non empty V35() V36() V37() V41() V42() V43() V128() V129() ext-real positive non negative V143() V144() V145() V146() V147() V148() V154() V156() ) Element of NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) * k : ( ( non empty ) ( non empty V35() V36() V37() V41() V42() V43() V128() V129() ext-real positive non negative V143() V144() V145() V146() V147() V148() V154() V156() ) Element of NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) ) : ( ( ) ( V35() V36() V37() V41() V42() V43() even V128() V129() ext-real non negative V143() V144() V145() V146() V147() V148() V156() ) Element of NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) + 1 : ( ( ) ( non empty V35() V36() V37() V41() V42() V43() V128() V129() ext-real positive non negative V143() V144() V145() V146() V147() V148() V154() V156() ) Element of NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) ) : ( ( ) ( non empty V35() V36() V37() V41() V42() V43() non even V128() V129() ext-real positive non negative V143() V144() V145() V146() V147() V148() V154() V156() ) Element of NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) ,m : ( ( ) ( V35() V36() V37() V41() V42() V43() V128() V129() ext-real non negative V143() V144() V145() V146() V147() V148() V156() ) Element of NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) ] : ( ( ) ( V15() ) Element of [:NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ,NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) :] : ( ( ) ( Relation-like non empty ) set ) ) in X : ( ( non empty finite ) ( Relation-like REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) -defined NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) -valued non empty finite ) Subset of ( ( ) ( non empty V107() cup-closed diff-closed preBoolean ) set ) ) ;

theorem :: HEYTING3:5
for m being ( ( ) ( V35() V36() V37() V41() V42() V43() V128() V129() ext-real non negative V143() V144() V145() V146() V147() V148() V156() ) Element of NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) )
for X being ( ( finite ) ( Relation-like REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) -defined NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) -valued finite ) Subset of ( ( ) ( non empty V107() cup-closed diff-closed preBoolean ) set ) ) ex k being ( ( ) ( V35() V36() V37() V41() V42() V43() V128() V129() ext-real non negative V143() V144() V145() V146() V147() V148() V156() ) Element of NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) st
for l being ( ( ) ( V35() V36() V37() V41() V42() V43() V128() V129() ext-real non negative V143() V144() V145() V146() V147() V148() V156() ) Element of NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) st l : ( ( ) ( V35() V36() V37() V41() V42() V43() V128() V129() ext-real non negative V143() V144() V145() V146() V147() V148() V156() ) Element of NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) >= k : ( ( ) ( V35() V36() V37() V41() V42() V43() V128() V129() ext-real non negative V143() V144() V145() V146() V147() V148() V156() ) Element of NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) holds
not [l : ( ( ) ( V35() V36() V37() V41() V42() V43() V128() V129() ext-real non negative V143() V144() V145() V146() V147() V148() V156() ) Element of NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) ,m : ( ( ) ( V35() V36() V37() V41() V42() V43() V128() V129() ext-real non negative V143() V144() V145() V146() V147() V148() V156() ) Element of NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) ] : ( ( ) ( V15() ) Element of [:NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ,NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) :] : ( ( ) ( Relation-like non empty ) set ) ) in X : ( ( finite ) ( Relation-like REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) -defined NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) -valued finite ) Subset of ( ( ) ( non empty V107() cup-closed diff-closed preBoolean ) set ) ) ;

theorem :: HEYTING3:6
for L being ( ( non empty Lattice-like upper-bounded ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like upper-bounded ) Lattice) holds Top L : ( ( non empty Lattice-like upper-bounded ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like upper-bounded ) Lattice) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty Lattice-like upper-bounded ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like upper-bounded ) Lattice) : ( ( ) ( non empty ) set ) ) = Top (LattPOSet L : ( ( non empty Lattice-like upper-bounded ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like upper-bounded ) Lattice) ) : ( ( strict reflexive transitive antisymmetric ) ( non empty strict reflexive transitive antisymmetric with_suprema with_infima upper-bounded ) RelStr ) : ( ( ) ( ) Element of the carrier of (LattPOSet b1 : ( ( non empty Lattice-like upper-bounded ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like upper-bounded ) Lattice) ) : ( ( strict reflexive transitive antisymmetric ) ( non empty strict reflexive transitive antisymmetric with_suprema with_infima upper-bounded ) RelStr ) : ( ( ) ( non empty ) set ) ) ;

theorem :: HEYTING3:7
for L being ( ( non empty Lattice-like lower-bounded ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded ) Lattice) holds Bottom L : ( ( non empty Lattice-like lower-bounded ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded ) Lattice) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty Lattice-like lower-bounded ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded ) Lattice) : ( ( ) ( non empty ) set ) ) = Bottom (LattPOSet L : ( ( non empty Lattice-like lower-bounded ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded ) Lattice) ) : ( ( strict reflexive transitive antisymmetric ) ( non empty strict reflexive transitive antisymmetric with_suprema with_infima lower-bounded ) RelStr ) : ( ( ) ( ) Element of the carrier of (LattPOSet b1 : ( ( non empty Lattice-like lower-bounded ) ( non empty join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded ) Lattice) ) : ( ( strict reflexive transitive antisymmetric ) ( non empty strict reflexive transitive antisymmetric with_suprema with_infima lower-bounded ) RelStr ) : ( ( ) ( non empty ) set ) ) ;

begin

theorem :: HEYTING3:8
for V being ( ( ) ( ) set )
for C being ( ( finite ) ( finite ) set )
for A, B being ( ( ) ( finite ) Element of Fin (PFuncs (V : ( ( ) ( ) set ) ,C : ( ( finite ) ( finite ) set ) )) : ( ( ) ( functional non empty ) set ) : ( ( preBoolean ) ( non empty cup-closed diff-closed preBoolean ) set ) ) st A : ( ( ) ( finite ) Element of Fin (PFuncs (b1 : ( ( ) ( ) set ) ,b2 : ( ( finite ) ( finite ) set ) )) : ( ( ) ( functional non empty ) set ) : ( ( preBoolean ) ( non empty cup-closed diff-closed preBoolean ) set ) ) = {} : ( ( ) ( Relation-like non-empty empty-yielding functional empty V35() V36() V37() V39() V40() V41() finite finite-yielding V48() FinSequence-like FinSequence-membered ext-real non positive non negative V143() V144() V145() V146() V147() V148() V149() V156() V157() V158() V159() ) set ) & B : ( ( ) ( finite ) Element of Fin (PFuncs (b1 : ( ( ) ( ) set ) ,b2 : ( ( finite ) ( finite ) set ) )) : ( ( ) ( functional non empty ) set ) : ( ( preBoolean ) ( non empty cup-closed diff-closed preBoolean ) set ) ) <> {} : ( ( ) ( Relation-like non-empty empty-yielding functional empty V35() V36() V37() V39() V40() V41() finite finite-yielding V48() FinSequence-like FinSequence-membered ext-real non positive non negative V143() V144() V145() V146() V147() V148() V149() V156() V157() V158() V159() ) set ) holds
B : ( ( ) ( finite ) Element of Fin (PFuncs (b1 : ( ( ) ( ) set ) ,b2 : ( ( finite ) ( finite ) set ) )) : ( ( ) ( functional non empty ) set ) : ( ( preBoolean ) ( non empty cup-closed diff-closed preBoolean ) set ) ) =>> A : ( ( ) ( finite ) Element of Fin (PFuncs (b1 : ( ( ) ( ) set ) ,b2 : ( ( finite ) ( finite ) set ) )) : ( ( ) ( functional non empty ) set ) : ( ( preBoolean ) ( non empty cup-closed diff-closed preBoolean ) set ) ) : ( ( ) ( finite ) Element of Fin (PFuncs (b1 : ( ( ) ( ) set ) ,b2 : ( ( finite ) ( finite ) set ) )) : ( ( ) ( functional non empty ) set ) : ( ( preBoolean ) ( non empty cup-closed diff-closed preBoolean ) set ) ) = {} : ( ( ) ( Relation-like non-empty empty-yielding functional empty V35() V36() V37() V39() V40() V41() finite finite-yielding V48() FinSequence-like FinSequence-membered ext-real non positive non negative V143() V144() V145() V146() V147() V148() V149() V156() V157() V158() V159() ) set ) ;

theorem :: HEYTING3:9
for V, V9, C, C9 being ( ( ) ( ) set ) st V : ( ( ) ( ) set ) c= V9 : ( ( ) ( ) set ) & C : ( ( ) ( ) set ) c= C9 : ( ( ) ( ) set ) holds
SubstitutionSet (V : ( ( ) ( ) set ) ,C : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) Element of bool (Fin (PFuncs (b1 : ( ( ) ( ) set ) ,b3 : ( ( ) ( ) set ) )) : ( ( ) ( functional non empty ) set ) ) : ( ( preBoolean ) ( non empty cup-closed diff-closed preBoolean ) set ) : ( ( ) ( non empty V107() cup-closed diff-closed preBoolean ) set ) ) c= SubstitutionSet (V9 : ( ( ) ( ) set ) ,C9 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) Element of bool (Fin (PFuncs (b2 : ( ( ) ( ) set ) ,b4 : ( ( ) ( ) set ) )) : ( ( ) ( functional non empty ) set ) ) : ( ( preBoolean ) ( non empty cup-closed diff-closed preBoolean ) set ) : ( ( ) ( non empty V107() cup-closed diff-closed preBoolean ) set ) ) ;

theorem :: HEYTING3:10
for V, V9, C, C9 being ( ( ) ( ) set )
for A being ( ( ) ( finite ) Element of Fin (PFuncs (V : ( ( ) ( ) set ) ,C : ( ( ) ( ) set ) )) : ( ( ) ( functional non empty ) set ) : ( ( preBoolean ) ( non empty cup-closed diff-closed preBoolean ) set ) )
for B being ( ( ) ( finite ) Element of Fin (PFuncs (V9 : ( ( ) ( ) set ) ,C9 : ( ( ) ( ) set ) )) : ( ( ) ( functional non empty ) set ) : ( ( preBoolean ) ( non empty cup-closed diff-closed preBoolean ) set ) ) st V : ( ( ) ( ) set ) c= V9 : ( ( ) ( ) set ) & C : ( ( ) ( ) set ) c= C9 : ( ( ) ( ) set ) & A : ( ( ) ( finite ) Element of Fin (PFuncs (b1 : ( ( ) ( ) set ) ,b3 : ( ( ) ( ) set ) )) : ( ( ) ( functional non empty ) set ) : ( ( preBoolean ) ( non empty cup-closed diff-closed preBoolean ) set ) ) = B : ( ( ) ( finite ) Element of Fin (PFuncs (b2 : ( ( ) ( ) set ) ,b4 : ( ( ) ( ) set ) )) : ( ( ) ( functional non empty ) set ) : ( ( preBoolean ) ( non empty cup-closed diff-closed preBoolean ) set ) ) holds
mi A : ( ( ) ( finite ) Element of Fin (PFuncs (b1 : ( ( ) ( ) set ) ,b3 : ( ( ) ( ) set ) )) : ( ( ) ( functional non empty ) set ) : ( ( preBoolean ) ( non empty cup-closed diff-closed preBoolean ) set ) ) : ( ( ) ( functional finite ) Element of SubstitutionSet (b1 : ( ( ) ( ) set ) ,b3 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) Element of bool (Fin (PFuncs (b1 : ( ( ) ( ) set ) ,b3 : ( ( ) ( ) set ) )) : ( ( ) ( functional non empty ) set ) ) : ( ( preBoolean ) ( non empty cup-closed diff-closed preBoolean ) set ) : ( ( ) ( non empty V107() cup-closed diff-closed preBoolean ) set ) ) ) = mi B : ( ( ) ( finite ) Element of Fin (PFuncs (b2 : ( ( ) ( ) set ) ,b4 : ( ( ) ( ) set ) )) : ( ( ) ( functional non empty ) set ) : ( ( preBoolean ) ( non empty cup-closed diff-closed preBoolean ) set ) ) : ( ( ) ( functional finite ) Element of SubstitutionSet (b2 : ( ( ) ( ) set ) ,b4 : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) Element of bool (Fin (PFuncs (b2 : ( ( ) ( ) set ) ,b4 : ( ( ) ( ) set ) )) : ( ( ) ( functional non empty ) set ) ) : ( ( preBoolean ) ( non empty cup-closed diff-closed preBoolean ) set ) : ( ( ) ( non empty V107() cup-closed diff-closed preBoolean ) set ) ) ) ;

theorem :: HEYTING3:11
for V, V9, C, C9 being ( ( ) ( ) set ) st V : ( ( ) ( ) set ) c= V9 : ( ( ) ( ) set ) & C : ( ( ) ( ) set ) c= C9 : ( ( ) ( ) set ) holds
the L_join of (SubstLatt (V : ( ( ) ( ) set ) ,C : ( ( ) ( ) set ) )) : ( ( strict ) ( non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V99() ) LattStr ) : ( ( Function-like V18([: the carrier of (SubstLatt (b1 : ( ( ) ( ) set ) ,b3 : ( ( ) ( ) set ) )) : ( ( strict ) ( non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V99() ) LattStr ) : ( ( ) ( non empty ) set ) , the carrier of (SubstLatt (b1 : ( ( ) ( ) set ) ,b3 : ( ( ) ( ) set ) )) : ( ( strict ) ( non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V99() ) LattStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like non empty ) set ) , the carrier of (SubstLatt (b1 : ( ( ) ( ) set ) ,b3 : ( ( ) ( ) set ) )) : ( ( strict ) ( non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V99() ) LattStr ) : ( ( ) ( non empty ) set ) ) ) ( Relation-like [: the carrier of (SubstLatt (b1 : ( ( ) ( ) set ) ,b3 : ( ( ) ( ) set ) )) : ( ( strict ) ( non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V99() ) LattStr ) : ( ( ) ( non empty ) set ) , the carrier of (SubstLatt (b1 : ( ( ) ( ) set ) ,b3 : ( ( ) ( ) set ) )) : ( ( strict ) ( non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V99() ) LattStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like non empty ) set ) -defined the carrier of (SubstLatt (b1 : ( ( ) ( ) set ) ,b3 : ( ( ) ( ) set ) )) : ( ( strict ) ( non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V99() ) LattStr ) : ( ( ) ( non empty ) set ) -valued Function-like V18([: the carrier of (SubstLatt (b1 : ( ( ) ( ) set ) ,b3 : ( ( ) ( ) set ) )) : ( ( strict ) ( non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V99() ) LattStr ) : ( ( ) ( non empty ) set ) , the carrier of (SubstLatt (b1 : ( ( ) ( ) set ) ,b3 : ( ( ) ( ) set ) )) : ( ( strict ) ( non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V99() ) LattStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like non empty ) set ) , the carrier of (SubstLatt (b1 : ( ( ) ( ) set ) ,b3 : ( ( ) ( ) set ) )) : ( ( strict ) ( non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V99() ) LattStr ) : ( ( ) ( non empty ) set ) ) ) Element of bool [:[: the carrier of (SubstLatt (b1 : ( ( ) ( ) set ) ,b3 : ( ( ) ( ) set ) )) : ( ( strict ) ( non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V99() ) LattStr ) : ( ( ) ( non empty ) set ) , the carrier of (SubstLatt (b1 : ( ( ) ( ) set ) ,b3 : ( ( ) ( ) set ) )) : ( ( strict ) ( non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V99() ) LattStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like non empty ) set ) , the carrier of (SubstLatt (b1 : ( ( ) ( ) set ) ,b3 : ( ( ) ( ) set ) )) : ( ( strict ) ( non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V99() ) LattStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like non empty ) set ) : ( ( ) ( non empty V107() cup-closed diff-closed preBoolean ) set ) ) = the L_join of (SubstLatt (V9 : ( ( ) ( ) set ) ,C9 : ( ( ) ( ) set ) )) : ( ( strict ) ( non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V99() ) LattStr ) : ( ( Function-like V18([: the carrier of (SubstLatt (b2 : ( ( ) ( ) set ) ,b4 : ( ( ) ( ) set ) )) : ( ( strict ) ( non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V99() ) LattStr ) : ( ( ) ( non empty ) set ) , the carrier of (SubstLatt (b2 : ( ( ) ( ) set ) ,b4 : ( ( ) ( ) set ) )) : ( ( strict ) ( non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V99() ) LattStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like non empty ) set ) , the carrier of (SubstLatt (b2 : ( ( ) ( ) set ) ,b4 : ( ( ) ( ) set ) )) : ( ( strict ) ( non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V99() ) LattStr ) : ( ( ) ( non empty ) set ) ) ) ( Relation-like [: the carrier of (SubstLatt (b2 : ( ( ) ( ) set ) ,b4 : ( ( ) ( ) set ) )) : ( ( strict ) ( non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V99() ) LattStr ) : ( ( ) ( non empty ) set ) , the carrier of (SubstLatt (b2 : ( ( ) ( ) set ) ,b4 : ( ( ) ( ) set ) )) : ( ( strict ) ( non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V99() ) LattStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like non empty ) set ) -defined the carrier of (SubstLatt (b2 : ( ( ) ( ) set ) ,b4 : ( ( ) ( ) set ) )) : ( ( strict ) ( non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V99() ) LattStr ) : ( ( ) ( non empty ) set ) -valued Function-like V18([: the carrier of (SubstLatt (b2 : ( ( ) ( ) set ) ,b4 : ( ( ) ( ) set ) )) : ( ( strict ) ( non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V99() ) LattStr ) : ( ( ) ( non empty ) set ) , the carrier of (SubstLatt (b2 : ( ( ) ( ) set ) ,b4 : ( ( ) ( ) set ) )) : ( ( strict ) ( non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V99() ) LattStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like non empty ) set ) , the carrier of (SubstLatt (b2 : ( ( ) ( ) set ) ,b4 : ( ( ) ( ) set ) )) : ( ( strict ) ( non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V99() ) LattStr ) : ( ( ) ( non empty ) set ) ) ) Element of bool [:[: the carrier of (SubstLatt (b2 : ( ( ) ( ) set ) ,b4 : ( ( ) ( ) set ) )) : ( ( strict ) ( non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V99() ) LattStr ) : ( ( ) ( non empty ) set ) , the carrier of (SubstLatt (b2 : ( ( ) ( ) set ) ,b4 : ( ( ) ( ) set ) )) : ( ( strict ) ( non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V99() ) LattStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like non empty ) set ) , the carrier of (SubstLatt (b2 : ( ( ) ( ) set ) ,b4 : ( ( ) ( ) set ) )) : ( ( strict ) ( non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V99() ) LattStr ) : ( ( ) ( non empty ) set ) :] : ( ( ) ( Relation-like non empty ) set ) : ( ( ) ( non empty V107() cup-closed diff-closed preBoolean ) set ) ) || the carrier of (SubstLatt (V : ( ( ) ( ) set ) ,C : ( ( ) ( ) set ) )) : ( ( strict ) ( non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V99() ) LattStr ) : ( ( ) ( non empty ) set ) : ( ( ) ( Relation-like Function-like ) set ) ;

definition
let V, C be ( ( ) ( ) set ) ;
func SubstPoset (V,C) -> ( ( ) ( ) RelStr ) equals :: HEYTING3:def 1
 LattPOSet (SubstLatt (V : ( ( ) ( ) set ) ,C : ( ( ) ( ) set ) )) : ( ( strict ) ( non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V99() ) LattStr ) : ( ( strict reflexive transitive antisymmetric ) ( non empty strict reflexive transitive antisymmetric with_suprema with_infima lower-bounded upper-bounded V118() ) RelStr ) ;
end;

registration
let V, C be ( ( ) ( ) set ) ;
cluster SubstPoset (V : ( ( ) ( ) set ) ,C : ( ( ) ( ) set ) ) : ( ( ) ( ) RelStr ) -> with_suprema with_infima ;
end;

registration
let V, C be ( ( ) ( ) set ) ;
cluster SubstPoset (V : ( ( ) ( ) set ) ,C : ( ( ) ( ) set ) ) : ( ( ) ( non empty with_suprema with_infima ) RelStr ) -> reflexive transitive antisymmetric ;
end;

theorem :: HEYTING3:12
for V, C being ( ( ) ( ) set )
for a, b being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds
( a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) <= b : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) iff for x being ( ( ) ( ) set ) st x : ( ( ) ( ) set ) in a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds
ex y being ( ( ) ( ) set ) st
( y : ( ( ) ( ) set ) in b : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) & y : ( ( ) ( ) set ) c= x : ( ( ) ( ) set ) ) ) ;

theorem :: HEYTING3:13
for V, V9, C, C9 being ( ( ) ( ) set ) st V : ( ( ) ( ) set ) c= V9 : ( ( ) ( ) set ) & C : ( ( ) ( ) set ) c= C9 : ( ( ) ( ) set ) holds
SubstPoset (V : ( ( ) ( ) set ) ,C : ( ( ) ( ) set ) ) : ( ( ) ( non empty reflexive transitive antisymmetric with_suprema with_infima ) RelStr ) is ( ( full ) ( reflexive transitive antisymmetric full ) SubRelStr of SubstPoset (V9 : ( ( ) ( ) set ) ,C9 : ( ( ) ( ) set ) ) : ( ( ) ( non empty reflexive transitive antisymmetric with_suprema with_infima ) RelStr ) ) ;

definition
let n, k be ( ( ) ( V35() V36() V37() V41() V42() V43() V128() V129() ext-real non negative V143() V144() V145() V146() V147() V148() V156() ) Element of NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) ;
func PFArt (n,k) -> ( ( ) ( ) Element of PFuncs (NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ,{k : ( ( ) ( ) set ) } : ( ( ) ( non empty finite V143() V144() V145() V146() V147() V148() V154() V155() V156() V157() V158() ) Element of bool NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) : ( ( ) ( non empty V107() cup-closed diff-closed preBoolean ) set ) ) ) : ( ( ) ( functional non empty ) set ) ) means :: HEYTING3:def 2
 for x being ( ( ) ( ) set ) holds
( x : ( ( ) ( ) set ) in it : ( ( ) ( ) Element of n : ( ( ) ( ) set ) ) iff ( ex m being ( ( odd ) ( non empty V35() V36() V37() V41() V42() V43() odd V128() V129() ext-real positive non negative V143() V144() V145() V146() V147() V148() V154() V156() ) Element of NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) st
( m : ( ( odd ) ( non empty V35() V36() V37() V41() V42() V43() odd V128() V129() ext-real positive non negative V143() V144() V145() V146() V147() V148() V154() V156() ) Element of NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) <= 2 : ( ( ) ( non empty V35() V36() V37() V41() V42() V43() V128() V129() ext-real positive non negative V143() V144() V145() V146() V147() V148() V154() V156() ) Element of NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) * n : ( ( ) ( ) set ) : ( ( ) ( V35() V36() V37() V41() V42() V43() V128() V129() ext-real non negative V143() V144() V145() V146() V147() V148() V156() ) Element of NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) & [m : ( ( odd ) ( non empty V35() V36() V37() V41() V42() V43() odd V128() V129() ext-real positive non negative V143() V144() V145() V146() V147() V148() V154() V156() ) Element of NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) ,k : ( ( ) ( ) set ) ] : ( ( ) ( V15() ) Element of [:NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ,NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) :] : ( ( ) ( Relation-like non empty ) set ) ) = x : ( ( ) ( ) set ) ) or [(2 : ( ( ) ( non empty V35() V36() V37() V41() V42() V43() V128() V129() ext-real positive non negative V143() V144() V145() V146() V147() V148() V154() V156() ) Element of NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) * n : ( ( ) ( ) set ) ) : ( ( ) ( V35() V36() V37() V41() V42() V43() V128() V129() ext-real non negative V143() V144() V145() V146() V147() V148() V156() ) Element of NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) ,k : ( ( ) ( ) set ) ] : ( ( ) ( V15() ) Element of [:NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ,NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) :] : ( ( ) ( Relation-like non empty ) set ) ) = x : ( ( ) ( ) set ) ) );
end;

registration
let n, k be ( ( ) ( V35() V36() V37() V41() V42() V43() V128() V129() ext-real non negative V143() V144() V145() V146() V147() V148() V156() ) Element of NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) ;
cluster PFArt (n : ( ( ) ( V35() V36() V37() V41() V42() V43() V128() V129() ext-real non negative V143() V144() V145() V146() V147() V148() V156() ) Element of NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) ,k : ( ( ) ( V35() V36() V37() V41() V42() V43() V128() V129() ext-real non negative V143() V144() V145() V146() V147() V148() V156() ) Element of NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) ) : ( ( ) ( ) Element of PFuncs (NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ,{k : ( ( ) ( V35() V36() V37() V41() V42() V43() V128() V129() ext-real non negative V143() V144() V145() V146() V147() V148() V156() ) Element of NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) } : ( ( ) ( non empty finite V143() V144() V145() V146() V147() V148() V154() V155() V156() V157() V158() ) Element of bool NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) : ( ( ) ( non empty V107() cup-closed diff-closed preBoolean ) set ) ) ) : ( ( ) ( functional non empty ) set ) ) -> finite ;
end;

definition
let n, k be ( ( ) ( V35() V36() V37() V41() V42() V43() V128() V129() ext-real non negative V143() V144() V145() V146() V147() V148() V156() ) Element of NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) ;
func PFCrt (n,k) -> ( ( ) ( ) Element of PFuncs (NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ,{k : ( ( ) ( ) set ) } : ( ( ) ( non empty finite V143() V144() V145() V146() V147() V148() V154() V155() V156() V157() V158() ) Element of bool NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) : ( ( ) ( non empty V107() cup-closed diff-closed preBoolean ) set ) ) ) : ( ( ) ( functional non empty ) set ) ) means :: HEYTING3:def 3
 for x being ( ( ) ( ) set ) holds
( x : ( ( ) ( ) set ) in it : ( ( ) ( ) Element of n : ( ( ) ( ) set ) ) iff ex m being ( ( odd ) ( non empty V35() V36() V37() V41() V42() V43() odd V128() V129() ext-real positive non negative V143() V144() V145() V146() V147() V148() V154() V156() ) Element of NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) st
( m : ( ( odd ) ( non empty V35() V36() V37() V41() V42() V43() odd V128() V129() ext-real positive non negative V143() V144() V145() V146() V147() V148() V154() V156() ) Element of NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) <= (2 : ( ( ) ( non empty V35() V36() V37() V41() V42() V43() V128() V129() ext-real positive non negative V143() V144() V145() V146() V147() V148() V154() V156() ) Element of NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) * n : ( ( ) ( ) set ) ) : ( ( ) ( V35() V36() V37() V41() V42() V43() V128() V129() ext-real non negative V143() V144() V145() V146() V147() V148() V156() ) Element of NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) + 1 : ( ( ) ( non empty V35() V36() V37() V41() V42() V43() V128() V129() ext-real positive non negative V143() V144() V145() V146() V147() V148() V154() V156() ) Element of NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) : ( ( ) ( non empty V35() V36() V37() V41() V42() V43() V128() V129() ext-real positive non negative V143() V144() V145() V146() V147() V148() V154() V156() ) Element of NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) & [m : ( ( odd ) ( non empty V35() V36() V37() V41() V42() V43() odd V128() V129() ext-real positive non negative V143() V144() V145() V146() V147() V148() V154() V156() ) Element of NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) ,k : ( ( ) ( ) set ) ] : ( ( ) ( V15() ) Element of [:NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ,NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) :] : ( ( ) ( Relation-like non empty ) set ) ) = x : ( ( ) ( ) set ) ) );
end;

registration
let n, k be ( ( ) ( V35() V36() V37() V41() V42() V43() V128() V129() ext-real non negative V143() V144() V145() V146() V147() V148() V156() ) Element of NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) ;
cluster PFCrt (n : ( ( ) ( V35() V36() V37() V41() V42() V43() V128() V129() ext-real non negative V143() V144() V145() V146() V147() V148() V156() ) Element of NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) ,k : ( ( ) ( V35() V36() V37() V41() V42() V43() V128() V129() ext-real non negative V143() V144() V145() V146() V147() V148() V156() ) Element of NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) ) : ( ( ) ( ) Element of PFuncs (NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ,{k : ( ( ) ( V35() V36() V37() V41() V42() V43() V128() V129() ext-real non negative V143() V144() V145() V146() V147() V148() V156() ) Element of NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) } : ( ( ) ( non empty finite V143() V144() V145() V146() V147() V148() V154() V155() V156() V157() V158() ) Element of bool NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) : ( ( ) ( non empty V107() cup-closed diff-closed preBoolean ) set ) ) ) : ( ( ) ( functional non empty ) set ) ) -> finite ;
end;

theorem :: HEYTING3:14
for n, k being ( ( ) ( V35() V36() V37() V41() V42() V43() V128() V129() ext-real non negative V143() V144() V145() V146() V147() V148() V156() ) Element of NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) holds [((2 : ( ( ) ( non empty V35() V36() V37() V41() V42() V43() V128() V129() ext-real positive non negative V143() V144() V145() V146() V147() V148() V154() V156() ) Element of NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) * n : ( ( ) ( V35() V36() V37() V41() V42() V43() V128() V129() ext-real non negative V143() V144() V145() V146() V147() V148() V156() ) Element of NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) ) : ( ( ) ( V35() V36() V37() V41() V42() V43() even V128() V129() ext-real non negative V143() V144() V145() V146() V147() V148() V156() ) Element of NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) + 1 : ( ( ) ( non empty V35() V36() V37() V41() V42() V43() V128() V129() ext-real positive non negative V143() V144() V145() V146() V147() V148() V154() V156() ) Element of NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) ) : ( ( ) ( non empty V35() V36() V37() V41() V42() V43() non even V128() V129() ext-real positive non negative V143() V144() V145() V146() V147() V148() V154() V156() ) Element of NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) ,k : ( ( ) ( V35() V36() V37() V41() V42() V43() V128() V129() ext-real non negative V143() V144() V145() V146() V147() V148() V156() ) Element of NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) ] : ( ( ) ( V15() ) Element of [:NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ,NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) :] : ( ( ) ( Relation-like non empty ) set ) ) in PFCrt (n : ( ( ) ( V35() V36() V37() V41() V42() V43() V128() V129() ext-real non negative V143() V144() V145() V146() V147() V148() V156() ) Element of NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) ,k : ( ( ) ( V35() V36() V37() V41() V42() V43() V128() V129() ext-real non negative V143() V144() V145() V146() V147() V148() V156() ) Element of NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) ) : ( ( ) ( finite ) Element of PFuncs (NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ,{b2 : ( ( ) ( V35() V36() V37() V41() V42() V43() V128() V129() ext-real non negative V143() V144() V145() V146() V147() V148() V156() ) Element of NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) } : ( ( ) ( non empty finite V143() V144() V145() V146() V147() V148() V154() V155() V156() V157() V158() ) Element of bool NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) : ( ( ) ( non empty V107() cup-closed diff-closed preBoolean ) set ) ) ) : ( ( ) ( functional non empty ) set ) ) ;

theorem :: HEYTING3:15
for n, k being ( ( ) ( V35() V36() V37() V41() V42() V43() V128() V129() ext-real non negative V143() V144() V145() V146() V147() V148() V156() ) Element of NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) holds PFCrt (n : ( ( ) ( V35() V36() V37() V41() V42() V43() V128() V129() ext-real non negative V143() V144() V145() V146() V147() V148() V156() ) Element of NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) ,k : ( ( ) ( V35() V36() V37() V41() V42() V43() V128() V129() ext-real non negative V143() V144() V145() V146() V147() V148() V156() ) Element of NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) ) : ( ( ) ( finite ) Element of PFuncs (NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ,{b2 : ( ( ) ( V35() V36() V37() V41() V42() V43() V128() V129() ext-real non negative V143() V144() V145() V146() V147() V148() V156() ) Element of NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) } : ( ( ) ( non empty finite V143() V144() V145() V146() V147() V148() V154() V155() V156() V157() V158() ) Element of bool NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) : ( ( ) ( non empty V107() cup-closed diff-closed preBoolean ) set ) ) ) : ( ( ) ( functional non empty ) set ) ) misses {[((2 : ( ( ) ( non empty V35() V36() V37() V41() V42() V43() V128() V129() ext-real positive non negative V143() V144() V145() V146() V147() V148() V154() V156() ) Element of NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) * n : ( ( ) ( V35() V36() V37() V41() V42() V43() V128() V129() ext-real non negative V143() V144() V145() V146() V147() V148() V156() ) Element of NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) ) : ( ( ) ( V35() V36() V37() V41() V42() V43() even V128() V129() ext-real non negative V143() V144() V145() V146() V147() V148() V156() ) Element of NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) + 3 : ( ( ) ( non empty V35() V36() V37() V41() V42() V43() V128() V129() ext-real positive non negative V143() V144() V145() V146() V147() V148() V154() V156() ) Element of NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) ) : ( ( ) ( non empty V35() V36() V37() V41() V42() V43() V128() V129() ext-real positive non negative V143() V144() V145() V146() V147() V148() V154() V156() ) Element of NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) ,k : ( ( ) ( V35() V36() V37() V41() V42() V43() V128() V129() ext-real non negative V143() V144() V145() V146() V147() V148() V156() ) Element of NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) ] : ( ( ) ( V15() ) Element of [:NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ,NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) :] : ( ( ) ( Relation-like non empty ) set ) ) } : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) -defined NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) -valued non empty finite ) Element of bool [:NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ,NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) :] : ( ( ) ( Relation-like non empty ) set ) : ( ( ) ( non empty V107() cup-closed diff-closed preBoolean ) set ) ) ;

theorem :: HEYTING3:16
for n, k being ( ( ) ( V35() V36() V37() V41() V42() V43() V128() V129() ext-real non negative V143() V144() V145() V146() V147() V148() V156() ) Element of NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) holds PFCrt ((n : ( ( ) ( V35() V36() V37() V41() V42() V43() V128() V129() ext-real non negative V143() V144() V145() V146() V147() V148() V156() ) Element of NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) + 1 : ( ( ) ( non empty V35() V36() V37() V41() V42() V43() V128() V129() ext-real positive non negative V143() V144() V145() V146() V147() V148() V154() V156() ) Element of NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) ) : ( ( ) ( non empty V35() V36() V37() V41() V42() V43() V128() V129() ext-real positive non negative V143() V144() V145() V146() V147() V148() V154() V156() ) Element of NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) ,k : ( ( ) ( V35() V36() V37() V41() V42() V43() V128() V129() ext-real non negative V143() V144() V145() V146() V147() V148() V156() ) Element of NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) ) : ( ( ) ( finite ) Element of PFuncs (NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ,{b2 : ( ( ) ( V35() V36() V37() V41() V42() V43() V128() V129() ext-real non negative V143() V144() V145() V146() V147() V148() V156() ) Element of NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) } : ( ( ) ( non empty finite V143() V144() V145() V146() V147() V148() V154() V155() V156() V157() V158() ) Element of bool NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) : ( ( ) ( non empty V107() cup-closed diff-closed preBoolean ) set ) ) ) : ( ( ) ( functional non empty ) set ) ) = (PFCrt (n : ( ( ) ( V35() V36() V37() V41() V42() V43() V128() V129() ext-real non negative V143() V144() V145() V146() V147() V148() V156() ) Element of NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) ,k : ( ( ) ( V35() V36() V37() V41() V42() V43() V128() V129() ext-real non negative V143() V144() V145() V146() V147() V148() V156() ) Element of NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) )) : ( ( ) ( finite ) Element of PFuncs (NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ,{b2 : ( ( ) ( V35() V36() V37() V41() V42() V43() V128() V129() ext-real non negative V143() V144() V145() V146() V147() V148() V156() ) Element of NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) } : ( ( ) ( non empty finite V143() V144() V145() V146() V147() V148() V154() V155() V156() V157() V158() ) Element of bool NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) : ( ( ) ( non empty V107() cup-closed diff-closed preBoolean ) set ) ) ) : ( ( ) ( functional non empty ) set ) ) \/ {[((2 : ( ( ) ( non empty V35() V36() V37() V41() V42() V43() V128() V129() ext-real positive non negative V143() V144() V145() V146() V147() V148() V154() V156() ) Element of NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) * n : ( ( ) ( V35() V36() V37() V41() V42() V43() V128() V129() ext-real non negative V143() V144() V145() V146() V147() V148() V156() ) Element of NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) ) : ( ( ) ( V35() V36() V37() V41() V42() V43() even V128() V129() ext-real non negative V143() V144() V145() V146() V147() V148() V156() ) Element of NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) + 3 : ( ( ) ( non empty V35() V36() V37() V41() V42() V43() V128() V129() ext-real positive non negative V143() V144() V145() V146() V147() V148() V154() V156() ) Element of NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) ) : ( ( ) ( non empty V35() V36() V37() V41() V42() V43() V128() V129() ext-real positive non negative V143() V144() V145() V146() V147() V148() V154() V156() ) Element of NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) ,k : ( ( ) ( V35() V36() V37() V41() V42() V43() V128() V129() ext-real non negative V143() V144() V145() V146() V147() V148() V156() ) Element of NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) ] : ( ( ) ( V15() ) Element of [:NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ,NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) :] : ( ( ) ( Relation-like non empty ) set ) ) } : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) -defined NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) -valued non empty finite ) Element of bool [:NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ,NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) :] : ( ( ) ( Relation-like non empty ) set ) : ( ( ) ( non empty V107() cup-closed diff-closed preBoolean ) set ) ) : ( ( ) ( non empty finite ) set ) ;

theorem :: HEYTING3:17
for n, k being ( ( ) ( V35() V36() V37() V41() V42() V43() V128() V129() ext-real non negative V143() V144() V145() V146() V147() V148() V156() ) Element of NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) holds PFCrt (n : ( ( ) ( V35() V36() V37() V41() V42() V43() V128() V129() ext-real non negative V143() V144() V145() V146() V147() V148() V156() ) Element of NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) ,k : ( ( ) ( V35() V36() V37() V41() V42() V43() V128() V129() ext-real non negative V143() V144() V145() V146() V147() V148() V156() ) Element of NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) ) : ( ( ) ( finite ) Element of PFuncs (NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ,{b2 : ( ( ) ( V35() V36() V37() V41() V42() V43() V128() V129() ext-real non negative V143() V144() V145() V146() V147() V148() V156() ) Element of NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) } : ( ( ) ( non empty finite V143() V144() V145() V146() V147() V148() V154() V155() V156() V157() V158() ) Element of bool NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) : ( ( ) ( non empty V107() cup-closed diff-closed preBoolean ) set ) ) ) : ( ( ) ( functional non empty ) set ) ) c< PFCrt ((n : ( ( ) ( V35() V36() V37() V41() V42() V43() V128() V129() ext-real non negative V143() V144() V145() V146() V147() V148() V156() ) Element of NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) + 1 : ( ( ) ( non empty V35() V36() V37() V41() V42() V43() V128() V129() ext-real positive non negative V143() V144() V145() V146() V147() V148() V154() V156() ) Element of NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) ) : ( ( ) ( non empty V35() V36() V37() V41() V42() V43() V128() V129() ext-real positive non negative V143() V144() V145() V146() V147() V148() V154() V156() ) Element of NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) ,k : ( ( ) ( V35() V36() V37() V41() V42() V43() V128() V129() ext-real non negative V143() V144() V145() V146() V147() V148() V156() ) Element of NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) ) : ( ( ) ( finite ) Element of PFuncs (NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ,{b2 : ( ( ) ( V35() V36() V37() V41() V42() V43() V128() V129() ext-real non negative V143() V144() V145() V146() V147() V148() V156() ) Element of NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) } : ( ( ) ( non empty finite V143() V144() V145() V146() V147() V148() V154() V155() V156() V157() V158() ) Element of bool NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) : ( ( ) ( non empty V107() cup-closed diff-closed preBoolean ) set ) ) ) : ( ( ) ( functional non empty ) set ) ) ;

registration
let n, k be ( ( ) ( V35() V36() V37() V41() V42() V43() V128() V129() ext-real non negative V143() V144() V145() V146() V147() V148() V156() ) Element of NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) ;
cluster PFArt (n : ( ( ) ( V35() V36() V37() V41() V42() V43() V128() V129() ext-real non negative V143() V144() V145() V146() V147() V148() V156() ) Element of NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) ,k : ( ( ) ( V35() V36() V37() V41() V42() V43() V128() V129() ext-real non negative V143() V144() V145() V146() V147() V148() V156() ) Element of NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) ) : ( ( ) ( finite ) Element of PFuncs (NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ,{k : ( ( ) ( V35() V36() V37() V41() V42() V43() V128() V129() ext-real non negative V143() V144() V145() V146() V147() V148() V156() ) Element of NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) } : ( ( ) ( non empty finite V143() V144() V145() V146() V147() V148() V154() V155() V156() V157() V158() ) Element of bool NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) : ( ( ) ( non empty V107() cup-closed diff-closed preBoolean ) set ) ) ) : ( ( ) ( functional non empty ) set ) ) -> non empty ;
end;

theorem :: HEYTING3:18
for n, m, k being ( ( ) ( V35() V36() V37() V41() V42() V43() V128() V129() ext-real non negative V143() V144() V145() V146() V147() V148() V156() ) Element of NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) holds not PFArt (n : ( ( ) ( V35() V36() V37() V41() V42() V43() V128() V129() ext-real non negative V143() V144() V145() V146() V147() V148() V156() ) Element of NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) ,m : ( ( ) ( V35() V36() V37() V41() V42() V43() V128() V129() ext-real non negative V143() V144() V145() V146() V147() V148() V156() ) Element of NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) ) : ( ( ) ( non empty finite ) Element of PFuncs (NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ,{b2 : ( ( ) ( V35() V36() V37() V41() V42() V43() V128() V129() ext-real non negative V143() V144() V145() V146() V147() V148() V156() ) Element of NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) } : ( ( ) ( non empty finite V143() V144() V145() V146() V147() V148() V154() V155() V156() V157() V158() ) Element of bool NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) : ( ( ) ( non empty V107() cup-closed diff-closed preBoolean ) set ) ) ) : ( ( ) ( functional non empty ) set ) ) c= PFCrt (k : ( ( ) ( V35() V36() V37() V41() V42() V43() V128() V129() ext-real non negative V143() V144() V145() V146() V147() V148() V156() ) Element of NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) ,m : ( ( ) ( V35() V36() V37() V41() V42() V43() V128() V129() ext-real non negative V143() V144() V145() V146() V147() V148() V156() ) Element of NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) ) : ( ( ) ( finite ) Element of PFuncs (NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ,{b2 : ( ( ) ( V35() V36() V37() V41() V42() V43() V128() V129() ext-real non negative V143() V144() V145() V146() V147() V148() V156() ) Element of NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) } : ( ( ) ( non empty finite V143() V144() V145() V146() V147() V148() V154() V155() V156() V157() V158() ) Element of bool NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) : ( ( ) ( non empty V107() cup-closed diff-closed preBoolean ) set ) ) ) : ( ( ) ( functional non empty ) set ) ) ;

theorem :: HEYTING3:19
for n, m, k being ( ( ) ( V35() V36() V37() V41() V42() V43() V128() V129() ext-real non negative V143() V144() V145() V146() V147() V148() V156() ) Element of NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) st n : ( ( ) ( V35() V36() V37() V41() V42() V43() V128() V129() ext-real non negative V143() V144() V145() V146() V147() V148() V156() ) Element of NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) <= k : ( ( ) ( V35() V36() V37() V41() V42() V43() V128() V129() ext-real non negative V143() V144() V145() V146() V147() V148() V156() ) Element of NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) holds
PFCrt (n : ( ( ) ( V35() V36() V37() V41() V42() V43() V128() V129() ext-real non negative V143() V144() V145() V146() V147() V148() V156() ) Element of NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) ,m : ( ( ) ( V35() V36() V37() V41() V42() V43() V128() V129() ext-real non negative V143() V144() V145() V146() V147() V148() V156() ) Element of NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) ) : ( ( ) ( finite ) Element of PFuncs (NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ,{b2 : ( ( ) ( V35() V36() V37() V41() V42() V43() V128() V129() ext-real non negative V143() V144() V145() V146() V147() V148() V156() ) Element of NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) } : ( ( ) ( non empty finite V143() V144() V145() V146() V147() V148() V154() V155() V156() V157() V158() ) Element of bool NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) : ( ( ) ( non empty V107() cup-closed diff-closed preBoolean ) set ) ) ) : ( ( ) ( functional non empty ) set ) ) c= PFCrt (k : ( ( ) ( V35() V36() V37() V41() V42() V43() V128() V129() ext-real non negative V143() V144() V145() V146() V147() V148() V156() ) Element of NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) ,m : ( ( ) ( V35() V36() V37() V41() V42() V43() V128() V129() ext-real non negative V143() V144() V145() V146() V147() V148() V156() ) Element of NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) ) : ( ( ) ( finite ) Element of PFuncs (NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ,{b2 : ( ( ) ( V35() V36() V37() V41() V42() V43() V128() V129() ext-real non negative V143() V144() V145() V146() V147() V148() V156() ) Element of NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) } : ( ( ) ( non empty finite V143() V144() V145() V146() V147() V148() V154() V155() V156() V157() V158() ) Element of bool NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) : ( ( ) ( non empty V107() cup-closed diff-closed preBoolean ) set ) ) ) : ( ( ) ( functional non empty ) set ) ) ;

theorem :: HEYTING3:20
for n being ( ( ) ( V35() V36() V37() V41() V42() V43() V128() V129() ext-real non negative V143() V144() V145() V146() V147() V148() V156() ) Element of NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) holds PFArt (1 : ( ( ) ( non empty V35() V36() V37() V41() V42() V43() V128() V129() ext-real positive non negative V143() V144() V145() V146() V147() V148() V154() V156() ) Element of NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) ,n : ( ( ) ( V35() V36() V37() V41() V42() V43() V128() V129() ext-real non negative V143() V144() V145() V146() V147() V148() V156() ) Element of NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) ) : ( ( ) ( non empty finite ) Element of PFuncs (NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ,{b1 : ( ( ) ( V35() V36() V37() V41() V42() V43() V128() V129() ext-real non negative V143() V144() V145() V146() V147() V148() V156() ) Element of NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) } : ( ( ) ( non empty finite V143() V144() V145() V146() V147() V148() V154() V155() V156() V157() V158() ) Element of bool NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) : ( ( ) ( non empty V107() cup-closed diff-closed preBoolean ) set ) ) ) : ( ( ) ( functional non empty ) set ) ) = {[1 : ( ( ) ( non empty V35() V36() V37() V41() V42() V43() V128() V129() ext-real positive non negative V143() V144() V145() V146() V147() V148() V154() V156() ) Element of NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) ,n : ( ( ) ( V35() V36() V37() V41() V42() V43() V128() V129() ext-real non negative V143() V144() V145() V146() V147() V148() V156() ) Element of NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) ] : ( ( ) ( V15() ) Element of [:NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ,NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) :] : ( ( ) ( Relation-like non empty ) set ) ) ,[2 : ( ( ) ( non empty V35() V36() V37() V41() V42() V43() V128() V129() ext-real positive non negative V143() V144() V145() V146() V147() V148() V154() V156() ) Element of NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) ,n : ( ( ) ( V35() V36() V37() V41() V42() V43() V128() V129() ext-real non negative V143() V144() V145() V146() V147() V148() V156() ) Element of NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) ] : ( ( ) ( V15() ) Element of [:NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ,NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) :] : ( ( ) ( Relation-like non empty ) set ) ) } : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) -defined NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) -valued non empty finite ) Element of bool [:NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ,NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) :] : ( ( ) ( Relation-like non empty ) set ) : ( ( ) ( non empty V107() cup-closed diff-closed preBoolean ) set ) ) ;

definition
let n, k be ( ( ) ( V35() V36() V37() V41() V42() V43() V128() V129() ext-real non negative V143() V144() V145() V146() V147() V148() V156() ) Element of NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) ;
func PFBrt (n,k) -> ( ( ) ( finite ) Element of Fin (PFuncs (NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ,{k : ( ( ) ( ) set ) } : ( ( ) ( non empty finite V143() V144() V145() V146() V147() V148() V154() V155() V156() V157() V158() ) Element of bool NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) : ( ( ) ( non empty V107() cup-closed diff-closed preBoolean ) set ) ) )) : ( ( ) ( functional non empty ) set ) : ( ( preBoolean ) ( non empty cup-closed diff-closed preBoolean ) set ) ) means :: HEYTING3:def 4
 for x being ( ( ) ( ) set ) holds
( x : ( ( ) ( ) set ) in it : ( ( ) ( ) Element of n : ( ( ) ( ) set ) ) iff ( ex m being ( ( non empty ) ( non empty V35() V36() V37() V41() V42() V43() V128() V129() ext-real positive non negative V143() V144() V145() V146() V147() V148() V154() V156() ) Element of NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) st
( m : ( ( non empty ) ( non empty V35() V36() V37() V41() V42() V43() V128() V129() ext-real positive non negative V143() V144() V145() V146() V147() V148() V154() V156() ) Element of NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) <= n : ( ( ) ( ) set ) & x : ( ( ) ( ) set ) = PFArt (m : ( ( non empty ) ( non empty V35() V36() V37() V41() V42() V43() V128() V129() ext-real positive non negative V143() V144() V145() V146() V147() V148() V154() V156() ) Element of NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) ,k : ( ( ) ( ) set ) ) : ( ( ) ( ) Element of PFuncs (NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ,{k : ( ( ) ( ) set ) } : ( ( ) ( non empty finite V143() V144() V145() V146() V147() V148() V154() V155() V156() V157() V158() ) Element of bool NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) : ( ( ) ( non empty V107() cup-closed diff-closed preBoolean ) set ) ) ) : ( ( ) ( functional non empty ) set ) ) ) or x : ( ( ) ( ) set ) = PFCrt (n : ( ( ) ( ) set ) ,k : ( ( ) ( ) set ) ) : ( ( ) ( ) Element of PFuncs (NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ,{k : ( ( ) ( ) set ) } : ( ( ) ( non empty finite V143() V144() V145() V146() V147() V148() V154() V155() V156() V157() V158() ) Element of bool NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) : ( ( ) ( non empty V107() cup-closed diff-closed preBoolean ) set ) ) ) : ( ( ) ( functional non empty ) set ) ) ) );
end;

theorem :: HEYTING3:21
for n, k being ( ( ) ( V35() V36() V37() V41() V42() V43() V128() V129() ext-real non negative V143() V144() V145() V146() V147() V148() V156() ) Element of NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) )
for x being ( ( ) ( ) set ) st x : ( ( ) ( ) set ) in PFBrt ((n : ( ( ) ( V35() V36() V37() V41() V42() V43() V128() V129() ext-real non negative V143() V144() V145() V146() V147() V148() V156() ) Element of NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) + 1 : ( ( ) ( non empty V35() V36() V37() V41() V42() V43() V128() V129() ext-real positive non negative V143() V144() V145() V146() V147() V148() V154() V156() ) Element of NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) ) : ( ( ) ( non empty V35() V36() V37() V41() V42() V43() V128() V129() ext-real positive non negative V143() V144() V145() V146() V147() V148() V154() V156() ) Element of NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) ,k : ( ( ) ( V35() V36() V37() V41() V42() V43() V128() V129() ext-real non negative V143() V144() V145() V146() V147() V148() V156() ) Element of NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) ) : ( ( ) ( finite ) Element of Fin (PFuncs (NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ,{b2 : ( ( ) ( V35() V36() V37() V41() V42() V43() V128() V129() ext-real non negative V143() V144() V145() V146() V147() V148() V156() ) Element of NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) } : ( ( ) ( non empty finite V143() V144() V145() V146() V147() V148() V154() V155() V156() V157() V158() ) Element of bool NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) : ( ( ) ( non empty V107() cup-closed diff-closed preBoolean ) set ) ) )) : ( ( ) ( functional non empty ) set ) : ( ( preBoolean ) ( non empty cup-closed diff-closed preBoolean ) set ) ) holds
ex y being ( ( ) ( ) set ) st
( y : ( ( ) ( ) set ) in PFBrt (n : ( ( ) ( V35() V36() V37() V41() V42() V43() V128() V129() ext-real non negative V143() V144() V145() V146() V147() V148() V156() ) Element of NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) ,k : ( ( ) ( V35() V36() V37() V41() V42() V43() V128() V129() ext-real non negative V143() V144() V145() V146() V147() V148() V156() ) Element of NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) ) : ( ( ) ( finite ) Element of Fin (PFuncs (NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ,{b2 : ( ( ) ( V35() V36() V37() V41() V42() V43() V128() V129() ext-real non negative V143() V144() V145() V146() V147() V148() V156() ) Element of NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) } : ( ( ) ( non empty finite V143() V144() V145() V146() V147() V148() V154() V155() V156() V157() V158() ) Element of bool NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) : ( ( ) ( non empty V107() cup-closed diff-closed preBoolean ) set ) ) )) : ( ( ) ( functional non empty ) set ) : ( ( preBoolean ) ( non empty cup-closed diff-closed preBoolean ) set ) ) & y : ( ( ) ( ) set ) c= x : ( ( ) ( ) set ) ) ;

theorem :: HEYTING3:22
for n, k being ( ( ) ( V35() V36() V37() V41() V42() V43() V128() V129() ext-real non negative V143() V144() V145() V146() V147() V148() V156() ) Element of NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) holds not PFCrt (n : ( ( ) ( V35() V36() V37() V41() V42() V43() V128() V129() ext-real non negative V143() V144() V145() V146() V147() V148() V156() ) Element of NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) ,k : ( ( ) ( V35() V36() V37() V41() V42() V43() V128() V129() ext-real non negative V143() V144() V145() V146() V147() V148() V156() ) Element of NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) ) : ( ( ) ( finite ) Element of PFuncs (NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ,{b2 : ( ( ) ( V35() V36() V37() V41() V42() V43() V128() V129() ext-real non negative V143() V144() V145() V146() V147() V148() V156() ) Element of NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) } : ( ( ) ( non empty finite V143() V144() V145() V146() V147() V148() V154() V155() V156() V157() V158() ) Element of bool NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) : ( ( ) ( non empty V107() cup-closed diff-closed preBoolean ) set ) ) ) : ( ( ) ( functional non empty ) set ) ) in PFBrt ((n : ( ( ) ( V35() V36() V37() V41() V42() V43() V128() V129() ext-real non negative V143() V144() V145() V146() V147() V148() V156() ) Element of NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) + 1 : ( ( ) ( non empty V35() V36() V37() V41() V42() V43() V128() V129() ext-real positive non negative V143() V144() V145() V146() V147() V148() V154() V156() ) Element of NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) ) : ( ( ) ( non empty V35() V36() V37() V41() V42() V43() V128() V129() ext-real positive non negative V143() V144() V145() V146() V147() V148() V154() V156() ) Element of NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) ,k : ( ( ) ( V35() V36() V37() V41() V42() V43() V128() V129() ext-real non negative V143() V144() V145() V146() V147() V148() V156() ) Element of NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) ) : ( ( ) ( finite ) Element of Fin (PFuncs (NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ,{b2 : ( ( ) ( V35() V36() V37() V41() V42() V43() V128() V129() ext-real non negative V143() V144() V145() V146() V147() V148() V156() ) Element of NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) } : ( ( ) ( non empty finite V143() V144() V145() V146() V147() V148() V154() V155() V156() V157() V158() ) Element of bool NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) : ( ( ) ( non empty V107() cup-closed diff-closed preBoolean ) set ) ) )) : ( ( ) ( functional non empty ) set ) : ( ( preBoolean ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ;

theorem :: HEYTING3:23
for n, m, k being ( ( ) ( V35() V36() V37() V41() V42() V43() V128() V129() ext-real non negative V143() V144() V145() V146() V147() V148() V156() ) Element of NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) st PFArt (n : ( ( ) ( V35() V36() V37() V41() V42() V43() V128() V129() ext-real non negative V143() V144() V145() V146() V147() V148() V156() ) Element of NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) ,m : ( ( ) ( V35() V36() V37() V41() V42() V43() V128() V129() ext-real non negative V143() V144() V145() V146() V147() V148() V156() ) Element of NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) ) : ( ( ) ( non empty finite ) Element of PFuncs (NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ,{b2 : ( ( ) ( V35() V36() V37() V41() V42() V43() V128() V129() ext-real non negative V143() V144() V145() V146() V147() V148() V156() ) Element of NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) } : ( ( ) ( non empty finite V143() V144() V145() V146() V147() V148() V154() V155() V156() V157() V158() ) Element of bool NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) : ( ( ) ( non empty V107() cup-closed diff-closed preBoolean ) set ) ) ) : ( ( ) ( functional non empty ) set ) ) c= PFArt (k : ( ( ) ( V35() V36() V37() V41() V42() V43() V128() V129() ext-real non negative V143() V144() V145() V146() V147() V148() V156() ) Element of NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) ,m : ( ( ) ( V35() V36() V37() V41() V42() V43() V128() V129() ext-real non negative V143() V144() V145() V146() V147() V148() V156() ) Element of NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) ) : ( ( ) ( non empty finite ) Element of PFuncs (NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ,{b2 : ( ( ) ( V35() V36() V37() V41() V42() V43() V128() V129() ext-real non negative V143() V144() V145() V146() V147() V148() V156() ) Element of NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) } : ( ( ) ( non empty finite V143() V144() V145() V146() V147() V148() V154() V155() V156() V157() V158() ) Element of bool NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) : ( ( ) ( non empty V107() cup-closed diff-closed preBoolean ) set ) ) ) : ( ( ) ( functional non empty ) set ) ) holds
n : ( ( ) ( V35() V36() V37() V41() V42() V43() V128() V129() ext-real non negative V143() V144() V145() V146() V147() V148() V156() ) Element of NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) = k : ( ( ) ( V35() V36() V37() V41() V42() V43() V128() V129() ext-real non negative V143() V144() V145() V146() V147() V148() V156() ) Element of NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) ;

theorem :: HEYTING3:24
for n, m, k being ( ( ) ( V35() V36() V37() V41() V42() V43() V128() V129() ext-real non negative V143() V144() V145() V146() V147() V148() V156() ) Element of NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) holds
( PFCrt (n : ( ( ) ( V35() V36() V37() V41() V42() V43() V128() V129() ext-real non negative V143() V144() V145() V146() V147() V148() V156() ) Element of NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) ,m : ( ( ) ( V35() V36() V37() V41() V42() V43() V128() V129() ext-real non negative V143() V144() V145() V146() V147() V148() V156() ) Element of NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) ) : ( ( ) ( finite ) Element of PFuncs (NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ,{b2 : ( ( ) ( V35() V36() V37() V41() V42() V43() V128() V129() ext-real non negative V143() V144() V145() V146() V147() V148() V156() ) Element of NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) } : ( ( ) ( non empty finite V143() V144() V145() V146() V147() V148() V154() V155() V156() V157() V158() ) Element of bool NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) : ( ( ) ( non empty V107() cup-closed diff-closed preBoolean ) set ) ) ) : ( ( ) ( functional non empty ) set ) ) c= PFArt (k : ( ( ) ( V35() V36() V37() V41() V42() V43() V128() V129() ext-real non negative V143() V144() V145() V146() V147() V148() V156() ) Element of NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) ,m : ( ( ) ( V35() V36() V37() V41() V42() V43() V128() V129() ext-real non negative V143() V144() V145() V146() V147() V148() V156() ) Element of NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) ) : ( ( ) ( non empty finite ) Element of PFuncs (NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ,{b2 : ( ( ) ( V35() V36() V37() V41() V42() V43() V128() V129() ext-real non negative V143() V144() V145() V146() V147() V148() V156() ) Element of NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) } : ( ( ) ( non empty finite V143() V144() V145() V146() V147() V148() V154() V155() V156() V157() V158() ) Element of bool NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) : ( ( ) ( non empty V107() cup-closed diff-closed preBoolean ) set ) ) ) : ( ( ) ( functional non empty ) set ) ) iff n : ( ( ) ( V35() V36() V37() V41() V42() V43() V128() V129() ext-real non negative V143() V144() V145() V146() V147() V148() V156() ) Element of NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) < k : ( ( ) ( V35() V36() V37() V41() V42() V43() V128() V129() ext-real non negative V143() V144() V145() V146() V147() V148() V156() ) Element of NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) ) ;

begin

theorem :: HEYTING3:25
for n, k being ( ( ) ( V35() V36() V37() V41() V42() V43() V128() V129() ext-real non negative V143() V144() V145() V146() V147() V148() V156() ) Element of NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) holds PFBrt (n : ( ( ) ( V35() V36() V37() V41() V42() V43() V128() V129() ext-real non negative V143() V144() V145() V146() V147() V148() V156() ) Element of NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) ,k : ( ( ) ( V35() V36() V37() V41() V42() V43() V128() V129() ext-real non negative V143() V144() V145() V146() V147() V148() V156() ) Element of NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) ) : ( ( ) ( finite ) Element of Fin (PFuncs (NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ,{b2 : ( ( ) ( V35() V36() V37() V41() V42() V43() V128() V129() ext-real non negative V143() V144() V145() V146() V147() V148() V156() ) Element of NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) } : ( ( ) ( non empty finite V143() V144() V145() V146() V147() V148() V154() V155() V156() V157() V158() ) Element of bool NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) : ( ( ) ( non empty V107() cup-closed diff-closed preBoolean ) set ) ) )) : ( ( ) ( functional non empty ) set ) : ( ( preBoolean ) ( non empty cup-closed diff-closed preBoolean ) set ) ) is ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ;

definition
let k be ( ( ) ( V35() V36() V37() V41() V42() V43() V128() V129() ext-real non negative V143() V144() V145() V146() V147() V148() V156() ) Element of NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) ;
func PFDrt k -> ( ( ) ( ) Subset of ) means :: HEYTING3:def 5
 for x being ( ( ) ( ) set ) holds
( x : ( ( ) ( ) set ) in it : ( ( ) ( ) set ) iff ex n being ( ( non empty ) ( non empty V35() V36() V37() V41() V42() V43() V128() V129() ext-real positive non negative V143() V144() V145() V146() V147() V148() V154() V156() ) Element of NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) st x : ( ( ) ( ) set ) = PFBrt (n : ( ( non empty ) ( non empty V35() V36() V37() V41() V42() V43() V128() V129() ext-real positive non negative V143() V144() V145() V146() V147() V148() V154() V156() ) Element of NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) ,k : ( ( ) ( ) set ) ) : ( ( ) ( finite ) Element of Fin (PFuncs (NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ,{k : ( ( ) ( ) set ) } : ( ( ) ( non empty finite V143() V144() V145() V146() V147() V148() V154() V155() V156() V157() V158() ) Element of bool NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) : ( ( ) ( non empty V107() cup-closed diff-closed preBoolean ) set ) ) )) : ( ( ) ( functional non empty ) set ) : ( ( preBoolean ) ( non empty cup-closed diff-closed preBoolean ) set ) ) );
end;

theorem :: HEYTING3:26
for k being ( ( ) ( V35() V36() V37() V41() V42() V43() V128() V129() ext-real non negative V143() V144() V145() V146() V147() V148() V156() ) Element of NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) holds PFBrt (1 : ( ( ) ( non empty V35() V36() V37() V41() V42() V43() V128() V129() ext-real positive non negative V143() V144() V145() V146() V147() V148() V154() V156() ) Element of NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) ,k : ( ( ) ( V35() V36() V37() V41() V42() V43() V128() V129() ext-real non negative V143() V144() V145() V146() V147() V148() V156() ) Element of NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) ) : ( ( ) ( finite ) Element of Fin (PFuncs (NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ,{b1 : ( ( ) ( V35() V36() V37() V41() V42() V43() V128() V129() ext-real non negative V143() V144() V145() V146() V147() V148() V156() ) Element of NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) } : ( ( ) ( non empty finite V143() V144() V145() V146() V147() V148() V154() V155() V156() V157() V158() ) Element of bool NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) : ( ( ) ( non empty V107() cup-closed diff-closed preBoolean ) set ) ) )) : ( ( ) ( functional non empty ) set ) : ( ( preBoolean ) ( non empty cup-closed diff-closed preBoolean ) set ) ) = {(PFArt (1 : ( ( ) ( non empty V35() V36() V37() V41() V42() V43() V128() V129() ext-real positive non negative V143() V144() V145() V146() V147() V148() V154() V156() ) Element of NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) ,k : ( ( ) ( V35() V36() V37() V41() V42() V43() V128() V129() ext-real non negative V143() V144() V145() V146() V147() V148() V156() ) Element of NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) )) : ( ( ) ( non empty finite ) Element of PFuncs (NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ,{b1 : ( ( ) ( V35() V36() V37() V41() V42() V43() V128() V129() ext-real non negative V143() V144() V145() V146() V147() V148() V156() ) Element of NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) } : ( ( ) ( non empty finite V143() V144() V145() V146() V147() V148() V154() V155() V156() V157() V158() ) Element of bool NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) : ( ( ) ( non empty V107() cup-closed diff-closed preBoolean ) set ) ) ) : ( ( ) ( functional non empty ) set ) ) ,(PFCrt (1 : ( ( ) ( non empty V35() V36() V37() V41() V42() V43() V128() V129() ext-real positive non negative V143() V144() V145() V146() V147() V148() V154() V156() ) Element of NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) ,k : ( ( ) ( V35() V36() V37() V41() V42() V43() V128() V129() ext-real non negative V143() V144() V145() V146() V147() V148() V156() ) Element of NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) )) : ( ( ) ( finite ) Element of PFuncs (NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ,{b1 : ( ( ) ( V35() V36() V37() V41() V42() V43() V128() V129() ext-real non negative V143() V144() V145() V146() V147() V148() V156() ) Element of NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) } : ( ( ) ( non empty finite V143() V144() V145() V146() V147() V148() V154() V155() V156() V157() V158() ) Element of bool NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) : ( ( ) ( non empty V107() cup-closed diff-closed preBoolean ) set ) ) ) : ( ( ) ( functional non empty ) set ) ) } : ( ( ) ( non empty finite V48() ) Element of bool (PFuncs (NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ,{b1 : ( ( ) ( V35() V36() V37() V41() V42() V43() V128() V129() ext-real non negative V143() V144() V145() V146() V147() V148() V156() ) Element of NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) } : ( ( ) ( non empty finite V143() V144() V145() V146() V147() V148() V154() V155() V156() V157() V158() ) Element of bool NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) : ( ( ) ( non empty V107() cup-closed diff-closed preBoolean ) set ) ) )) : ( ( ) ( functional non empty ) set ) : ( ( ) ( non empty V107() cup-closed diff-closed preBoolean ) set ) ) ;

theorem :: HEYTING3:27
for k being ( ( ) ( V35() V36() V37() V41() V42() V43() V128() V129() ext-real non negative V143() V144() V145() V146() V147() V148() V156() ) Element of NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) holds PFBrt (1 : ( ( ) ( non empty V35() V36() V37() V41() V42() V43() V128() V129() ext-real positive non negative V143() V144() V145() V146() V147() V148() V154() V156() ) Element of NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) ,k : ( ( ) ( V35() V36() V37() V41() V42() V43() V128() V129() ext-real non negative V143() V144() V145() V146() V147() V148() V156() ) Element of NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) ) : ( ( ) ( finite ) Element of Fin (PFuncs (NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ,{b1 : ( ( ) ( V35() V36() V37() V41() V42() V43() V128() V129() ext-real non negative V143() V144() V145() V146() V147() V148() V156() ) Element of NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) } : ( ( ) ( non empty finite V143() V144() V145() V146() V147() V148() V154() V155() V156() V157() V158() ) Element of bool NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) : ( ( ) ( non empty V107() cup-closed diff-closed preBoolean ) set ) ) )) : ( ( ) ( functional non empty ) set ) : ( ( preBoolean ) ( non empty cup-closed diff-closed preBoolean ) set ) ) <> {{} : ( ( ) ( Relation-like non-empty empty-yielding functional empty V35() V36() V37() V39() V40() V41() finite finite-yielding V48() FinSequence-like FinSequence-membered ext-real non positive non negative V143() V144() V145() V146() V147() V148() V149() V156() V157() V158() V159() ) set ) } : ( ( ) ( non empty finite V48() V143() V144() V145() V146() V147() V148() V154() V155() V156() V157() V158() ) set ) ;

registration
let k be ( ( ) ( V35() V36() V37() V41() V42() V43() V128() V129() ext-real non negative V143() V144() V145() V146() V147() V148() V156() ) Element of NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) ;
cluster PFBrt (1 : ( ( ) ( non empty V35() V36() V37() V41() V42() V43() V128() V129() ext-real positive non negative V143() V144() V145() V146() V147() V148() V154() V156() ) Element of NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) ,k : ( ( ) ( V35() V36() V37() V41() V42() V43() V128() V129() ext-real non negative V143() V144() V145() V146() V147() V148() V156() ) Element of NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) ) : ( ( ) ( finite ) Element of Fin (PFuncs (NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ,{k : ( ( ) ( V35() V36() V37() V41() V42() V43() V128() V129() ext-real non negative V143() V144() V145() V146() V147() V148() V156() ) Element of NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) } : ( ( ) ( non empty finite V143() V144() V145() V146() V147() V148() V154() V155() V156() V157() V158() ) Element of bool NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) : ( ( ) ( non empty V107() cup-closed diff-closed preBoolean ) set ) ) )) : ( ( ) ( functional non empty ) set ) : ( ( preBoolean ) ( non empty cup-closed diff-closed preBoolean ) set ) ) -> non empty ;
end;

theorem :: HEYTING3:28
for n, k being ( ( ) ( V35() V36() V37() V41() V42() V43() V128() V129() ext-real non negative V143() V144() V145() V146() V147() V148() V156() ) Element of NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) holds {(PFArt (n : ( ( ) ( V35() V36() V37() V41() V42() V43() V128() V129() ext-real non negative V143() V144() V145() V146() V147() V148() V156() ) Element of NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) ,k : ( ( ) ( V35() V36() V37() V41() V42() V43() V128() V129() ext-real non negative V143() V144() V145() V146() V147() V148() V156() ) Element of NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) )) : ( ( ) ( non empty finite ) Element of PFuncs (NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ,{b2 : ( ( ) ( V35() V36() V37() V41() V42() V43() V128() V129() ext-real non negative V143() V144() V145() V146() V147() V148() V156() ) Element of NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) } : ( ( ) ( non empty finite V143() V144() V145() V146() V147() V148() V154() V155() V156() V157() V158() ) Element of bool NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) : ( ( ) ( non empty V107() cup-closed diff-closed preBoolean ) set ) ) ) : ( ( ) ( functional non empty ) set ) ) } : ( ( ) ( non empty finite V48() ) Element of bool (PFuncs (NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ,{b2 : ( ( ) ( V35() V36() V37() V41() V42() V43() V128() V129() ext-real non negative V143() V144() V145() V146() V147() V148() V156() ) Element of NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) } : ( ( ) ( non empty finite V143() V144() V145() V146() V147() V148() V154() V155() V156() V157() V158() ) Element of bool NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) : ( ( ) ( non empty V107() cup-closed diff-closed preBoolean ) set ) ) )) : ( ( ) ( functional non empty ) set ) : ( ( ) ( non empty V107() cup-closed diff-closed preBoolean ) set ) ) is ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ;

theorem :: HEYTING3:29
for k being ( ( ) ( V35() V36() V37() V41() V42() V43() V128() V129() ext-real non negative V143() V144() V145() V146() V147() V148() V156() ) Element of NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) )
for V, X being ( ( ) ( ) set )
for a being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) st X : ( ( ) ( ) set ) in a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds
X : ( ( ) ( ) set ) is ( ( finite ) ( Relation-like b2 : ( ( ) ( ) set ) -defined {b1 : ( ( ) ( V35() V36() V37() V41() V42() V43() V128() V129() ext-real non negative V143() V144() V145() V146() V147() V148() V156() ) Element of NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) } : ( ( ) ( non empty finite V143() V144() V145() V146() V147() V148() V154() V155() V156() V157() V158() ) Element of bool NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) : ( ( ) ( non empty V107() cup-closed diff-closed preBoolean ) set ) ) -valued finite ) Subset of ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ;

theorem :: HEYTING3:30
for m being ( ( ) ( V35() V36() V37() V41() V42() V43() V128() V129() ext-real non negative V143() V144() V145() V146() V147() V148() V156() ) Element of NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) )
for a being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) st PFDrt m : ( ( ) ( V35() V36() V37() V41() V42() V43() V128() V129() ext-real non negative V143() V144() V145() V146() V147() V148() V156() ) Element of NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) : ( ( ) ( ) Subset of ) is_>=_than a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds
for X being ( ( non empty ) ( non empty ) set ) st X : ( ( non empty ) ( non empty ) set ) in a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds
ex n being ( ( ) ( V35() V36() V37() V41() V42() V43() V128() V129() ext-real non negative V143() V144() V145() V146() V147() V148() V156() ) Element of NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) st
( [n : ( ( ) ( V35() V36() V37() V41() V42() V43() V128() V129() ext-real non negative V143() V144() V145() V146() V147() V148() V156() ) Element of NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) ,m : ( ( ) ( V35() V36() V37() V41() V42() V43() V128() V129() ext-real non negative V143() V144() V145() V146() V147() V148() V156() ) Element of NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) ] : ( ( ) ( V15() ) Element of [:NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ,NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) :] : ( ( ) ( Relation-like non empty ) set ) ) in X : ( ( non empty ) ( non empty ) set ) & not n : ( ( ) ( V35() V36() V37() V41() V42() V43() V128() V129() ext-real non negative V143() V144() V145() V146() V147() V148() V156() ) Element of NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) is odd ) ;

theorem :: HEYTING3:31
for k being ( ( ) ( V35() V36() V37() V41() V42() V43() V128() V129() ext-real non negative V143() V144() V145() V146() V147() V148() V156() ) Element of NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) )
for a, b being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) )
for X being ( ( ) ( ) Subset of ) st a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) is_<=_than X : ( ( ) ( ) Subset of ) & b : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) is_<=_than X : ( ( ) ( ) Subset of ) holds
a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) "\/" b : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of (SubstPoset (NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ,{b1 : ( ( ) ( V35() V36() V37() V41() V42() V43() V128() V129() ext-real non negative V143() V144() V145() V146() V147() V148() V156() ) Element of NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) } : ( ( ) ( non empty finite V143() V144() V145() V146() V147() V148() V154() V155() V156() V157() V158() ) Element of bool NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) : ( ( ) ( non empty V107() cup-closed diff-closed preBoolean ) set ) ) )) : ( ( ) ( non empty reflexive transitive antisymmetric with_suprema with_infima ) RelStr ) : ( ( ) ( non empty ) set ) ) is_<=_than X : ( ( ) ( ) Subset of ) ;

registration
let k be ( ( ) ( V35() V36() V37() V41() V42() V43() V128() V129() ext-real non negative V143() V144() V145() V146() V147() V148() V156() ) Element of NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) ;
cluster non empty for ( ( ) ( ) Element of the carrier of (SubstPoset (NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ,{k : ( ( ) ( V35() V36() V37() V41() V42() V43() V128() V129() ext-real non negative V143() V144() V145() V146() V147() V148() V156() ) Element of NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) } : ( ( ) ( non empty finite V143() V144() V145() V146() V147() V148() V154() V155() V156() V157() V158() ) Element of bool NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) : ( ( ) ( non empty V107() cup-closed diff-closed preBoolean ) set ) ) )) : ( ( ) ( non empty reflexive transitive antisymmetric with_suprema with_infima ) RelStr ) : ( ( ) ( non empty ) set ) ) ;
end;

theorem :: HEYTING3:32
for n being ( ( ) ( V35() V36() V37() V41() V42() V43() V128() V129() ext-real non negative V143() V144() V145() V146() V147() V148() V156() ) Element of NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) )
for a being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) st {} : ( ( ) ( Relation-like non-empty empty-yielding functional empty V35() V36() V37() V39() V40() V41() finite finite-yielding V48() FinSequence-like FinSequence-membered ext-real non positive non negative V143() V144() V145() V146() V147() V148() V149() V156() V157() V158() V159() ) set ) in a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds
a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) = {{} : ( ( ) ( Relation-like non-empty empty-yielding functional empty V35() V36() V37() V39() V40() V41() finite finite-yielding V48() FinSequence-like FinSequence-membered ext-real non positive non negative V143() V144() V145() V146() V147() V148() V149() V156() V157() V158() V159() ) set ) } : ( ( ) ( non empty finite V48() V143() V144() V145() V146() V147() V148() V154() V155() V156() V157() V158() ) set ) ;

theorem :: HEYTING3:33
for k being ( ( ) ( V35() V36() V37() V41() V42() V43() V128() V129() ext-real non negative V143() V144() V145() V146() V147() V148() V156() ) Element of NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) )
for a being ( ( non empty ) ( non empty ) Element of ( ( ) ( non empty ) set ) ) st a : ( ( non empty ) ( non empty ) Element of ( ( ) ( non empty ) set ) ) <> {{} : ( ( ) ( Relation-like non-empty empty-yielding functional empty V35() V36() V37() V39() V40() V41() finite finite-yielding V48() FinSequence-like FinSequence-membered ext-real non positive non negative V143() V144() V145() V146() V147() V148() V149() V156() V157() V158() V159() ) set ) } : ( ( ) ( non empty finite V48() V143() V144() V145() V146() V147() V148() V154() V155() V156() V157() V158() ) set ) holds
ex f being ( ( Relation-like Function-like finite ) ( Relation-like Function-like finite ) Function) st
( f : ( ( Relation-like Function-like finite ) ( Relation-like Function-like finite ) Function) in a : ( ( non empty ) ( non empty ) Element of ( ( ) ( non empty ) set ) ) & f : ( ( Relation-like Function-like finite ) ( Relation-like Function-like finite ) Function) <> {} : ( ( ) ( Relation-like non-empty empty-yielding functional empty V35() V36() V37() V39() V40() V41() finite finite-yielding V48() FinSequence-like FinSequence-membered ext-real non positive non negative V143() V144() V145() V146() V147() V148() V149() V156() V157() V158() V159() ) set ) ) ;

theorem :: HEYTING3:34
for k being ( ( ) ( V35() V36() V37() V41() V42() V43() V128() V129() ext-real non negative V143() V144() V145() V146() V147() V148() V156() ) Element of NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) )
for a being ( ( non empty ) ( non empty ) Element of ( ( ) ( non empty ) set ) )
for a9 being ( ( ) ( finite ) Element of Fin (PFuncs (NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ,{k : ( ( ) ( V35() V36() V37() V41() V42() V43() V128() V129() ext-real non negative V143() V144() V145() V146() V147() V148() V156() ) Element of NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) } : ( ( ) ( non empty finite V143() V144() V145() V146() V147() V148() V154() V155() V156() V157() V158() ) Element of bool NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) : ( ( ) ( non empty V107() cup-closed diff-closed preBoolean ) set ) ) )) : ( ( ) ( functional non empty ) set ) : ( ( preBoolean ) ( non empty cup-closed diff-closed preBoolean ) set ) ) st a : ( ( non empty ) ( non empty ) Element of ( ( ) ( non empty ) set ) ) <> {{} : ( ( ) ( Relation-like non-empty empty-yielding functional empty V35() V36() V37() V39() V40() V41() finite finite-yielding V48() FinSequence-like FinSequence-membered ext-real non positive non negative V143() V144() V145() V146() V147() V148() V149() V156() V157() V158() V159() ) set ) } : ( ( ) ( non empty finite V48() V143() V144() V145() V146() V147() V148() V154() V155() V156() V157() V158() ) set ) & a : ( ( non empty ) ( non empty ) Element of ( ( ) ( non empty ) set ) ) = a9 : ( ( ) ( finite ) Element of Fin (PFuncs (NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ,{b1 : ( ( ) ( V35() V36() V37() V41() V42() V43() V128() V129() ext-real non negative V143() V144() V145() V146() V147() V148() V156() ) Element of NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) } : ( ( ) ( non empty finite V143() V144() V145() V146() V147() V148() V154() V155() V156() V157() V158() ) Element of bool NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) : ( ( ) ( non empty V107() cup-closed diff-closed preBoolean ) set ) ) )) : ( ( ) ( functional non empty ) set ) : ( ( preBoolean ) ( non empty cup-closed diff-closed preBoolean ) set ) ) holds
Involved a9 : ( ( ) ( finite ) Element of Fin (PFuncs (NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ,{b1 : ( ( ) ( V35() V36() V37() V41() V42() V43() V128() V129() ext-real non negative V143() V144() V145() V146() V147() V148() V156() ) Element of NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) } : ( ( ) ( non empty finite V143() V144() V145() V146() V147() V148() V154() V155() V156() V157() V158() ) Element of bool NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) : ( ( ) ( non empty V107() cup-closed diff-closed preBoolean ) set ) ) )) : ( ( ) ( functional non empty ) set ) : ( ( preBoolean ) ( non empty cup-closed diff-closed preBoolean ) set ) ) : ( ( ) ( finite ) set ) is ( ( non empty finite ) ( non empty finite V143() V144() V145() V146() V147() V148() V154() V155() V156() V157() V158() ) Subset of ( ( ) ( non empty V107() cup-closed diff-closed preBoolean ) set ) ) ;

theorem :: HEYTING3:35
for k being ( ( ) ( V35() V36() V37() V41() V42() V43() V128() V129() ext-real non negative V143() V144() V145() V146() V147() V148() V156() ) Element of NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) )
for a being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) )
for a9 being ( ( ) ( finite ) Element of Fin (PFuncs (NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ,{k : ( ( ) ( V35() V36() V37() V41() V42() V43() V128() V129() ext-real non negative V143() V144() V145() V146() V147() V148() V156() ) Element of NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) } : ( ( ) ( non empty finite V143() V144() V145() V146() V147() V148() V154() V155() V156() V157() V158() ) Element of bool NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) : ( ( ) ( non empty V107() cup-closed diff-closed preBoolean ) set ) ) )) : ( ( ) ( functional non empty ) set ) : ( ( preBoolean ) ( non empty cup-closed diff-closed preBoolean ) set ) )
for B being ( ( non empty finite ) ( non empty finite V143() V144() V145() V146() V147() V148() V154() V155() V156() V157() V158() ) Subset of ( ( ) ( non empty V107() cup-closed diff-closed preBoolean ) set ) ) st B : ( ( non empty finite ) ( non empty finite V143() V144() V145() V146() V147() V148() V154() V155() V156() V157() V158() ) Subset of ( ( ) ( non empty V107() cup-closed diff-closed preBoolean ) set ) ) = Involved a9 : ( ( ) ( finite ) Element of Fin (PFuncs (NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ,{b1 : ( ( ) ( V35() V36() V37() V41() V42() V43() V128() V129() ext-real non negative V143() V144() V145() V146() V147() V148() V156() ) Element of NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) } : ( ( ) ( non empty finite V143() V144() V145() V146() V147() V148() V154() V155() V156() V157() V158() ) Element of bool NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) : ( ( ) ( non empty V107() cup-closed diff-closed preBoolean ) set ) ) )) : ( ( ) ( functional non empty ) set ) : ( ( preBoolean ) ( non empty cup-closed diff-closed preBoolean ) set ) ) : ( ( ) ( finite ) set ) & a9 : ( ( ) ( finite ) Element of Fin (PFuncs (NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ,{b1 : ( ( ) ( V35() V36() V37() V41() V42() V43() V128() V129() ext-real non negative V143() V144() V145() V146() V147() V148() V156() ) Element of NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) } : ( ( ) ( non empty finite V143() V144() V145() V146() V147() V148() V154() V155() V156() V157() V158() ) Element of bool NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) : ( ( ) ( non empty V107() cup-closed diff-closed preBoolean ) set ) ) )) : ( ( ) ( functional non empty ) set ) : ( ( preBoolean ) ( non empty cup-closed diff-closed preBoolean ) set ) ) = a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds
for X being ( ( ) ( ) set ) st X : ( ( ) ( ) set ) in a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds
for l being ( ( ) ( V35() V36() V37() V41() V42() V43() V128() V129() ext-real non negative V143() V144() V145() V146() V147() V148() V156() ) Element of NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) st l : ( ( ) ( V35() V36() V37() V41() V42() V43() V128() V129() ext-real non negative V143() V144() V145() V146() V147() V148() V156() ) Element of NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) > (max B : ( ( non empty finite ) ( non empty finite V143() V144() V145() V146() V147() V148() V154() V155() V156() V157() V158() ) Subset of ( ( ) ( non empty V107() cup-closed diff-closed preBoolean ) set ) ) ) : ( ( ext-real ) ( V35() V36() V37() V41() V42() V43() V128() ext-real non negative ) set ) + 1 : ( ( ) ( non empty V35() V36() V37() V41() V42() V43() V128() V129() ext-real positive non negative V143() V144() V145() V146() V147() V148() V154() V156() ) Element of NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) : ( ( ) ( non empty V35() V36() V37() V41() V42() V43() V128() V129() ext-real positive non negative V143() V144() V145() V146() V147() V148() V154() V156() ) Element of NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) holds
not [l : ( ( ) ( V35() V36() V37() V41() V42() V43() V128() V129() ext-real non negative V143() V144() V145() V146() V147() V148() V156() ) Element of NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) ,k : ( ( ) ( V35() V36() V37() V41() V42() V43() V128() V129() ext-real non negative V143() V144() V145() V146() V147() V148() V156() ) Element of NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) ] : ( ( ) ( V15() ) Element of [:NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ,NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) :] : ( ( ) ( Relation-like non empty ) set ) ) in X : ( ( ) ( ) set ) ;

theorem :: HEYTING3:36
for k being ( ( ) ( V35() V36() V37() V41() V42() V43() V128() V129() ext-real non negative V143() V144() V145() V146() V147() V148() V156() ) Element of NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) holds Top (SubstPoset (NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ,{k : ( ( ) ( V35() V36() V37() V41() V42() V43() V128() V129() ext-real non negative V143() V144() V145() V146() V147() V148() V156() ) Element of NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) } : ( ( ) ( non empty finite V143() V144() V145() V146() V147() V148() V154() V155() V156() V157() V158() ) Element of bool NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) : ( ( ) ( non empty V107() cup-closed diff-closed preBoolean ) set ) ) )) : ( ( ) ( non empty reflexive transitive antisymmetric with_suprema with_infima ) RelStr ) : ( ( ) ( ) Element of the carrier of (SubstPoset (NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ,{b1 : ( ( ) ( V35() V36() V37() V41() V42() V43() V128() V129() ext-real non negative V143() V144() V145() V146() V147() V148() V156() ) Element of NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) } : ( ( ) ( non empty finite V143() V144() V145() V146() V147() V148() V154() V155() V156() V157() V158() ) Element of bool NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) : ( ( ) ( non empty V107() cup-closed diff-closed preBoolean ) set ) ) )) : ( ( ) ( non empty reflexive transitive antisymmetric with_suprema with_infima ) RelStr ) : ( ( ) ( non empty ) set ) ) = {{} : ( ( ) ( Relation-like non-empty empty-yielding functional empty V35() V36() V37() V39() V40() V41() finite finite-yielding V48() FinSequence-like FinSequence-membered ext-real non positive non negative V143() V144() V145() V146() V147() V148() V149() V156() V157() V158() V159() ) set ) } : ( ( ) ( non empty finite V48() V143() V144() V145() V146() V147() V148() V154() V155() V156() V157() V158() ) set ) ;

theorem :: HEYTING3:37
for k being ( ( ) ( V35() V36() V37() V41() V42() V43() V128() V129() ext-real non negative V143() V144() V145() V146() V147() V148() V156() ) Element of NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) holds Bottom (SubstPoset (NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ,{k : ( ( ) ( V35() V36() V37() V41() V42() V43() V128() V129() ext-real non negative V143() V144() V145() V146() V147() V148() V156() ) Element of NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) } : ( ( ) ( non empty finite V143() V144() V145() V146() V147() V148() V154() V155() V156() V157() V158() ) Element of bool NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) : ( ( ) ( non empty V107() cup-closed diff-closed preBoolean ) set ) ) )) : ( ( ) ( non empty reflexive transitive antisymmetric with_suprema with_infima ) RelStr ) : ( ( ) ( ) Element of the carrier of (SubstPoset (NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ,{b1 : ( ( ) ( V35() V36() V37() V41() V42() V43() V128() V129() ext-real non negative V143() V144() V145() V146() V147() V148() V156() ) Element of NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) } : ( ( ) ( non empty finite V143() V144() V145() V146() V147() V148() V154() V155() V156() V157() V158() ) Element of bool NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) : ( ( ) ( non empty V107() cup-closed diff-closed preBoolean ) set ) ) )) : ( ( ) ( non empty reflexive transitive antisymmetric with_suprema with_infima ) RelStr ) : ( ( ) ( non empty ) set ) ) = {} : ( ( ) ( Relation-like non-empty empty-yielding functional empty V35() V36() V37() V39() V40() V41() finite finite-yielding V48() FinSequence-like FinSequence-membered ext-real non positive non negative V143() V144() V145() V146() V147() V148() V149() V156() V157() V158() V159() ) set ) ;

theorem :: HEYTING3:38
for k being ( ( ) ( V35() V36() V37() V41() V42() V43() V128() V129() ext-real non negative V143() V144() V145() V146() V147() V148() V156() ) Element of NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) )
for a, b being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) st a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) <= b : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) & a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) = {{} : ( ( ) ( Relation-like non-empty empty-yielding functional empty V35() V36() V37() V39() V40() V41() finite finite-yielding V48() FinSequence-like FinSequence-membered ext-real non positive non negative V143() V144() V145() V146() V147() V148() V149() V156() V157() V158() V159() ) set ) } : ( ( ) ( non empty finite V48() V143() V144() V145() V146() V147() V148() V154() V155() V156() V157() V158() ) set ) holds
b : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) = {{} : ( ( ) ( Relation-like non-empty empty-yielding functional empty V35() V36() V37() V39() V40() V41() finite finite-yielding V48() FinSequence-like FinSequence-membered ext-real non positive non negative V143() V144() V145() V146() V147() V148() V149() V156() V157() V158() V159() ) set ) } : ( ( ) ( non empty finite V48() V143() V144() V145() V146() V147() V148() V154() V155() V156() V157() V158() ) set ) ;

theorem :: HEYTING3:39
for k being ( ( ) ( V35() V36() V37() V41() V42() V43() V128() V129() ext-real non negative V143() V144() V145() V146() V147() V148() V156() ) Element of NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) )
for a, b being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) st a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) <= b : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) & b : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) = {} : ( ( ) ( Relation-like non-empty empty-yielding functional empty V35() V36() V37() V39() V40() V41() finite finite-yielding V48() FinSequence-like FinSequence-membered ext-real non positive non negative V143() V144() V145() V146() V147() V148() V149() V156() V157() V158() V159() ) set ) holds
a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) = {} : ( ( ) ( Relation-like non-empty empty-yielding functional empty V35() V36() V37() V39() V40() V41() finite finite-yielding V48() FinSequence-like FinSequence-membered ext-real non positive non negative V143() V144() V145() V146() V147() V148() V149() V156() V157() V158() V159() ) set ) ;

theorem :: HEYTING3:40
for m being ( ( ) ( V35() V36() V37() V41() V42() V43() V128() V129() ext-real non negative V143() V144() V145() V146() V147() V148() V156() ) Element of NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) )
for a being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) st PFDrt m : ( ( ) ( V35() V36() V37() V41() V42() V43() V128() V129() ext-real non negative V143() V144() V145() V146() V147() V148() V156() ) Element of NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) : ( ( ) ( ) Subset of ) is_>=_than a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds
a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) <> {{} : ( ( ) ( Relation-like non-empty empty-yielding functional empty V35() V36() V37() V39() V40() V41() finite finite-yielding V48() FinSequence-like FinSequence-membered ext-real non positive non negative V143() V144() V145() V146() V147() V148() V149() V156() V157() V158() V159() ) set ) } : ( ( ) ( non empty finite V48() V143() V144() V145() V146() V147() V148() V154() V155() V156() V157() V158() ) set ) ;

registration
let m be ( ( ) ( V35() V36() V37() V41() V42() V43() V128() V129() ext-real non negative V143() V144() V145() V146() V147() V148() V156() ) Element of NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) ;
cluster SubstPoset (NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ,{m : ( ( ) ( V35() V36() V37() V41() V42() V43() V128() V129() ext-real non negative V143() V144() V145() V146() V147() V148() V156() ) Element of NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) } : ( ( ) ( non empty finite V143() V144() V145() V146() V147() V148() V154() V155() V156() V157() V158() ) Element of bool NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) : ( ( ) ( non empty V107() cup-closed diff-closed preBoolean ) set ) ) ) : ( ( ) ( non empty reflexive transitive antisymmetric with_suprema with_infima ) RelStr ) -> non complete ;
end;

registration
let m be ( ( ) ( V35() V36() V37() V41() V42() V43() V128() V129() ext-real non negative V143() V144() V145() V146() V147() V148() V156() ) Element of NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) ;
cluster SubstLatt (NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ,{m : ( ( ) ( V35() V36() V37() V41() V42() V43() V128() V129() ext-real non negative V143() V144() V145() V146() V147() V148() V156() ) Element of NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) ) } : ( ( ) ( non empty finite V143() V144() V145() V146() V147() V148() V154() V155() V156() V157() V158() ) Element of bool NAT : ( ( ) ( non empty V35() V36() V37() V143() V144() V145() V146() V147() V148() V149() V154() V156() ) Element of bool REAL : ( ( ) ( V143() V144() V145() V149() V156() V157() V159() ) set ) : ( ( ) ( non empty cup-closed diff-closed preBoolean ) set ) ) : ( ( ) ( non empty V107() cup-closed diff-closed preBoolean ) set ) ) ) : ( ( strict ) ( non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like distributive modular lower-bounded upper-bounded V99() ) LattStr ) -> strict non complete ;
end;