let k be natural Number ; :: thesis: ( not k < 2 or k = 0 or k = 1 )
assume k < 2 ; :: thesis: ( k = 0 or k = 1 )
then k < 1 + 1 ;
hence ( k = 0 or k = 1 ) by Th14, Th22; :: thesis: verum