let i be object ; :: according to PBOOLE:def 13 :: thesis: ( not i in the carrier of S or not (InvCl R) . i is empty )
assume i in the carrier of S ; :: thesis: not (InvCl R) . i is empty
then reconsider s = i as SortSymbol of S ;
set x = the Element of R . s;
R c= InvCl R by Def11;
then A1: R . s c= (InvCl R) . s ;
the Element of R . s in R . s ;
hence not (InvCl R) . i is empty by A1; :: thesis: verum