let A be Circuit of X,S; :: thesis: ( A is gate`2=den & A is non-empty )
thus A is gate`2=den by Def10; :: thesis: A is non-empty
( not the Sorts of A is empty & the Sorts of A is constant & the_value_of the Sorts of A = X ) by Def10;
then ( dom the Sorts of A = the carrier of S & ( for i being set st i in dom the Sorts of A holds
not the Sorts of A . i is empty ) ) by FUNCT_1:def 18, PARTFUN1:def 4;
then the Sorts of A is non-empty by PBOOLE:def 16;
hence A is non-empty by MSUALG_1:def 8; :: thesis: verum