let C be Component of the Sorts of A; :: thesis: not C is empty
ex i being object st
( i in the carrier of S & C = the Sorts of A . i ) by PBOOLE:138;
hence not C is empty ; :: thesis: verum