take id L ; :: thesis: id L is kernel
thus id L is projection ; :: according to WAYBEL_1:def 15 :: thesis: id L <= id L
thus id L <= id L by Lm1; :: thesis: verum