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