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 #) ; :: thesis: ( 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 ) ; :: thesis: verum