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