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