take l2_Space ; :: thesis: l2_Space is complete
thus l2_Space is complete ; :: thesis: verum