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