set a1 = the non empty set ;
set a2 = the non empty set ;
set a3 = the Subset of the non empty set ;
set a4 = the Function of [: the non empty set , the non empty set :], the non empty set ;
set a5 = the Function of the non empty set , the non empty set ;
set a6 = the Function of the non empty set , the non empty set ;
take
StackSystem(# the non empty set , the non empty set , the Subset of the non empty set , the Function of [: the non empty set , the non empty set :], the non empty set , the Function of the non empty set , the non empty set , the Function of the non empty set , the non empty set #)
; ( not StackSystem(# the non empty set , the non empty set , the Subset of the non empty set , the Function of [: the non empty set , the non empty set :], the non empty set , the Function of the non empty set , the non empty set , the Function of the non empty set , the non empty set #) is empty & not StackSystem(# the non empty set , the non empty set , the Subset of the non empty set , the Function of [: the non empty set , the non empty set :], the non empty set , the Function of the non empty set , the non empty set , the Function of the non empty set , the non empty set #) is void & StackSystem(# the non empty set , the non empty set , the Subset of the non empty set , the Function of [: the non empty set , the non empty set :], the non empty set , the Function of the non empty set , the non empty set , the Function of the non empty set , the non empty set #) is strict )
thus
( not StackSystem(# the non empty set , the non empty set , the Subset of the non empty set , the Function of [: the non empty set , the non empty set :], the non empty set , the Function of the non empty set , the non empty set , the Function of the non empty set , the non empty set #) is empty & not StackSystem(# the non empty set , the non empty set , the Subset of the non empty set , the Function of [: the non empty set , the non empty set :], the non empty set , the Function of the non empty set , the non empty set , the Function of the non empty set , the non empty set #) is void & StackSystem(# the non empty set , the non empty set , the Subset of the non empty set , the Function of [: the non empty set , the non empty set :], the non empty set , the Function of the non empty set , the non empty set , the Function of the non empty set , the non empty set #) is strict )
; verum