take 1GateCircuit p,f ; :: thesis: ( 1GateCircuit p,f is gate`2=den & 1GateCircuit p,f is strict & 1GateCircuit p,f is non-empty )
thus ( 1GateCircuit p,f is gate`2=den & 1GateCircuit p,f is strict & 1GateCircuit p,f is non-empty ) ; :: thesis: verum