take l1_Space ; :: thesis: l1_Space is complete
thus l1_Space is complete by Def16, RSSPACE3:11; :: thesis: verum