let c1, x1, x2, x3, x4, y1, y2, y3, y4, c2, c3, c4, c5, n1, n2, n3, n4, n, c5b be set ; :: thesis: ( ( not MAJ3 x1,y1,c1 is empty implies not c2 is empty ) & ( not MAJ3 x2,y2,c2 is empty implies not c3 is empty ) & ( not MAJ3 x3,y3,c3 is empty implies not c4 is empty ) & ( not MAJ3 x4,y4,c4 is empty implies not c5 is empty ) & ( not n1 is empty implies not OR2 x1,y1 is empty ) & ( not n2 is empty implies not OR2 x2,y2 is empty ) & ( not n3 is empty implies not OR2 x3,y3 is empty ) & ( not n4 is empty implies not OR2 x4,y4 is empty ) & ( not n is empty implies not AND5 c1,n1,n2,n3,n4 is empty ) & ( not c5b is empty implies not OR2 c5,n is empty ) & ( not OR2 c5,n is empty implies not c5b is empty ) implies ( not c5 is empty iff not c5b is empty ) )
assume that
A1: ( ( not MAJ3 x1,y1,c1 is empty implies not c2 is empty ) & ( not MAJ3 x2,y2,c2 is empty implies not c3 is empty ) & ( not MAJ3 x3,y3,c3 is empty implies not c4 is empty ) ) and
A2: ( not MAJ3 x4,y4,c4 is empty implies not c5 is empty ) and
A3: ( not n1 is empty implies not OR2 x1,y1 is empty ) and
A4: ( not n2 is empty implies not OR2 x2,y2 is empty ) and
A5: ( not n3 is empty implies not OR2 x3,y3 is empty ) and
A6: ( not n4 is empty implies not OR2 x4,y4 is empty ) and
A7: ( not n is empty implies not AND5 c1,n1,n2,n3,n4 is empty ) and
A8: ( not c5b is empty implies not OR2 c5,n is empty ) and
A9: ( not OR2 c5,n is empty implies not c5b is empty ) ; :: thesis: ( not c5 is empty iff not c5b is empty )

A10: now

assume A11: not n is empty ; :: thesis: not MAJ3 x4,y4,c4 is empty
then A12: not c1 is empty by A7, Def18;
A13: ( not x3 is empty or not y3 is empty ) by A5, A7, A11, Def18;
A14: ( not x2 is empty or not y2 is empty ) by A4, A7, A11, Def18;
A15: ( not x4 is empty or not y4 is empty ) by A6, A7, A11, Def18;
( not x1 is empty or not y1 is empty ) by A3, A7, A11, Def18;
hence not MAJ3 x4,y4,c4 is empty by A1, A12, A14, A13, A15; :: thesis: verum

end;

thus ( not c5 is empty implies not c5b is empty ) by A9; :: thesis: ( not c5b is empty implies not c5 is empty )
assume not c5b is empty ; :: thesis: not c5 is empty
hence not c5 is empty by A2, A8, A10; :: thesis: verum