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