take StandardStackSystem the non empty set ; :: thesis: ( StandardStackSystem the non empty set is pop-finite & StandardStackSystem the non empty set is push-pop & StandardStackSystem the non empty set is top-push & StandardStackSystem the non empty set is pop-push & StandardStackSystem the non empty set is push-non-empty & StandardStackSystem the non empty set is strict )
thus ( StandardStackSystem the non empty set is pop-finite & StandardStackSystem the non empty set is push-pop & StandardStackSystem the non empty set is top-push & StandardStackSystem the non empty set is pop-push & StandardStackSystem the non empty set is push-non-empty & StandardStackSystem the non empty set is strict ) ; :: thesis: verum