let S be locally_directed OrderSortedSign; :: thesis: for X being V5() ManySortedSet of holds PTVars X is non-empty
let X be V5() ManySortedSet of ; :: thesis: PTVars X is non-empty
let x be set ; :: according to PBOOLE:def 16 :: thesis: ( not x in the carrier of S or not (PTVars X) . x is empty )
assume x in the carrier of S ; :: thesis: not (PTVars X) . x is empty
then reconsider s = x as Element of S ;
(PTVars X) . s = PTVars s,X by Def25;
hence not (PTVars X) . x is empty ; :: thesis: verum