let k be non trivial Nat; :: thesis: k >= 2
k >= 1 by NAT_1:14;
then ( k > 1 or k = 1 ) by XXREAL_0:1;
then k >= 1 + 1 by Def1, NAT_1:13;
hence k >= 2 ; :: thesis: verum