thus id L is idempotent by YELLOW_2:21; :: according to WAYBEL_1:def 13 :: thesis: id L is monotone
thus id L is monotone ; :: thesis: verum