take id L ; :: thesis: id L is projection
thus id L is projection ; :: thesis: verum