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