A1: ( l = 0 or l = 1 ) by XBOOLEAN:def 3;
( k = 0 or k = 1 ) by XBOOLEAN:def 3;
hence ( k <= l iff k => l = TRUE ) by A1; :: thesis: verum