let i be set ; :: according to PBOOLE:def 16 :: thesis: ( not i in the carrier of S or not (StabCl R) . i is empty )
assume i in the carrier of S ; :: thesis: not (StabCl R) . i is empty
then reconsider s = i as SortSymbol of S ;
consider x being Element of R . s;
R c= StabCl R by Def12;
then ( x in R . s & R . s c= (StabCl R) . s ) by PBOOLE:def 5;
hence not (StabCl R) . i is empty ; :: thesis: verum