Char F = 0 by REALALG1:28;
then QS F is prepositive_cone by T0;
hence QS F is negative-disjoint ; :: thesis: verum