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