consider f being set , p being FinSequence;
take 1GateCircStr (p,f) ; :: thesis: ( 1GateCircStr (p,f) is unsplit & 1GateCircStr (p,f) is gate`1=arity & not 1GateCircStr (p,f) is void & 1GateCircStr (p,f) is strict & not 1GateCircStr (p,f) is empty )
thus ( 1GateCircStr (p,f) is unsplit & 1GateCircStr (p,f) is gate`1=arity & not 1GateCircStr (p,f) is void & 1GateCircStr (p,f) is strict & not 1GateCircStr (p,f) is empty ) ; :: thesis: verum