take 1_No ; :: thesis: 1_No is positive
thus 1_No is positive ; :: thesis: verum