let x be object ; :: according to PBOOLE:def 13 :: thesis: ( not x in the carrier of S or not (SORTS A) . x is empty )
assume x in the carrier of S ; :: thesis: not (SORTS A) . x is empty
then reconsider s = x as SortSymbol of S ;
(SORTS A) . s = product (Carrier (A,s)) by Def10;
hence not (SORTS A) . x is empty ; :: thesis: verum