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 ) )
thus ( ( 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 ) ) :: thesis: verum
proof
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 :: thesis: ( not n is empty implies not MAJ3 (x4,y4,c4) is empty )
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
end;