let A be Circuit of S; :: thesis: ( A is one-gate implies ( A is strict & A is non-empty ) )
assume A is one-gate ; :: thesis: ( A is strict & A is non-empty )
then ex X being non empty finite set ex n being Element of NAT ex p being FinSeqLen of n ex f being Function of (n -tuples_on X),X st
( S = 1GateCircStr (p,f) & A = 1GateCircuit (p,f) ) by Def7;
hence ( A is strict & A is non-empty ) ; :: thesis: verum