let i be object ; :: according to PBOOLE:def 13 :: thesis: ( not i in the carrier of S or not (ParsedTerms X) . i is empty )
assume i in the carrier of S ; :: thesis: not (ParsedTerms X) . i is empty
then reconsider s = i as Element of S ;
(ParsedTerms X) . s = ParsedTerms (X,s) by Def8;
hence not (ParsedTerms X) . i is empty ; :: thesis: verum