let P be Preordering of F; :: thesis: ( P is maximal implies P is spanning )
assume P is maximal ; :: thesis: P is spanning
then P is positive_cone by T1;
hence P is spanning ; :: thesis: verum