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