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