set S = 1GateCircStr p,f;
let i be set ; :: according to FINSET_1:def 4,MSAFREE2:def 11 :: thesis: ( not i in the carrier of (1GateCircStr p,f) or the Sorts of (1GateCircuit p,f) . i is finite )
assume i in the carrier of (1GateCircStr p,f) ; :: thesis: the Sorts of (1GateCircuit p,f) . i is finite
hence the Sorts of (1GateCircuit p,f) . i is finite by Th62; :: thesis: verum