the carrier of (1GateCircStr (p,f,x)) = (rng p) \/ {x} by Def5;
hence not the carrier of (1GateCircStr (p,f,x)) is empty ; :: according to STRUCT_0:def 1 :: thesis: verum