set s = {1};
take {1} ; :: thesis: ( not {1} is empty & {1} is without_zero )
thus not {1} is empty ; :: thesis: {1} is without_zero
thus {1} is without_zero ; :: thesis: verum