ex A being Circuit of S st
( the Sorts of A is constant & the_value_of the Sorts of A = X & A is gate`2=den ) by Def9;
hence ex b<sub>1</sub> being Circuit of S st
( b<sub>1</sub> is gate`2=den & the Sorts of b₁ is constant & the_value_of the Sorts of b₁ = X ) ; :: thesis: verum