let j, l be Nat; :: thesis: ( l <= j or l = j + 1 or j + 2 <= l )
A1: (j + 1) + 1 = j + 2 ;
( l < j + 1 or l = j + 1 or j + 1 < l ) by XXREAL_0:1;
hence ( l <= j or l = j + 1 or j + 2 <= l ) by A1, NAT_1:13; :: thesis: verum