let i be set ; :: according to PBOOLE:def 16 :: thesis: ( not i in the carrier of S or not (FreeSort X) . i is empty )
assume i in the carrier of S ; :: thesis: not (FreeSort X) . i is empty
then reconsider s = i as SortSymbol of S ;
(FreeSort X) . s = FreeSort X,s by Def13;
hence not (FreeSort X) . i is empty ; :: thesis: verum