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