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