take l1_Space ; :: thesis: not l1_Space is trivial
thus not l1_Space is trivial ; :: thesis: verum