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
A1: dom the Sorts of A = the carrier of S by PARTFUN1:def 4;
( not the Sorts of A is empty & the Sorts of A is constant & the_value_of the Sorts of A = X ) by Def10;
then 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;
then the Sorts of A is non-empty by A1, PBOOLE:def 16;
hence A is non-empty by MSUALG_1:def 8; :: thesis: verum