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