let x, y, c be object ; for f being Function of (2 -tuples_on BOOLEAN),BOOLEAN holds
( [<*x,y*>,f] in the carrier of (2GatesCircStr (x,y,c,f)) & [<*[<*x,y*>,f],c*>,f] in the carrier of (2GatesCircStr (x,y,c,f)) )
let f be Function of (2 -tuples_on BOOLEAN),BOOLEAN; ( [<*x,y*>,f] in the carrier of (2GatesCircStr (x,y,c,f)) & [<*[<*x,y*>,f],c*>,f] in the carrier of (2GatesCircStr (x,y,c,f)) )
set S1 = 1GateCircStr (<*x,y*>,f);
set S2 = 1GateCircStr (<*[<*x,y*>,f],c*>,f);
( [<*x,y*>,f] in the carrier of (1GateCircStr (<*x,y*>,f)) & [<*[<*x,y*>,f],c*>,f] in the carrier of (1GateCircStr (<*[<*x,y*>,f],c*>,f)) )
by Th43;
hence
( [<*x,y*>,f] in the carrier of (2GatesCircStr (x,y,c,f)) & [<*[<*x,y*>,f],c*>,f] in the carrier of (2GatesCircStr (x,y,c,f)) )
by Th20; verum