take 0 ; :: thesis: 0 is empty
thus 0 is empty ; :: thesis: verum