take {0 } ; :: thesis: {0 } is right_end
thus {0 } is right_end ; :: thesis: verum