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