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

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 )

assume not c5b is empty ; :: thesis: not c5 is empty

hence not c5 is empty by A2, A8, A10; :: thesis: verum

end;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 )

thus
( not c5 is empty implies not c5b is empty )
by A9; :: thesis: ( not c5b is empty implies not c5 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;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

assume not c5b is empty ; :: thesis: not c5 is empty

hence not c5 is empty by A2, A8, A10; :: thesis: verum