let i be object ; :: according to PBOOLE:def 13 :: 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 Def11;

hence not (FreeSort X) . i is empty ; :: thesis: verum

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 Def11;

hence not (FreeSort X) . i is empty ; :: thesis: verum