let s0, s1, s2, s3, s4, s5, s6, s7, ns0, ns1, ns2, ns3, ns4, ns5, ns6, ns7, q1, q2, q3, nq1, nq2, nq3 be set ; :: thesis: not ( ( not s0 is empty implies not AND3 ((NOT1 q3),(NOT1 q2),(NOT1 q1)) is empty ) & ( not AND3 ((NOT1 q3),(NOT1 q2),(NOT1 q1)) is empty implies not s0 is empty ) & ( not s1 is empty implies not AND3 ((NOT1 q3),(NOT1 q2),q1) is empty ) & ( not AND3 ((NOT1 q3),(NOT1 q2),q1) is empty implies not s1 is empty ) & ( not s2 is empty implies not AND3 ((NOT1 q3),q2,(NOT1 q1)) is empty ) & ( not AND3 ((NOT1 q3),q2,(NOT1 q1)) is empty implies not s2 is empty ) & ( not s3 is empty implies not AND3 ((NOT1 q3),q2,q1) is empty ) & ( not AND3 ((NOT1 q3),q2,q1) is empty implies not s3 is empty ) & ( not s4 is empty implies not AND3 (q3,(NOT1 q2),(NOT1 q1)) is empty ) & ( not AND3 (q3,(NOT1 q2),(NOT1 q1)) is empty implies not s4 is empty ) & ( not s5 is empty implies not AND3 (q3,(NOT1 q2),q1) is empty ) & ( not AND3 (q3,(NOT1 q2),q1) is empty implies not s5 is empty ) & ( not s6 is empty implies not AND3 (q3,q2,(NOT1 q1)) is empty ) & ( not AND3 (q3,q2,(NOT1 q1)) is empty implies not s6 is empty ) & ( not s7 is empty implies not AND3 (q3,q2,q1) is empty ) & ( not AND3 (q3,q2,q1) is empty implies not s7 is empty ) & ( not ns0 is empty implies not AND3 ((NOT1 nq3),(NOT1 nq2),(NOT1 nq1)) is empty ) & ( not AND3 ((NOT1 nq3),(NOT1 nq2),(NOT1 nq1)) is empty implies not ns0 is empty ) & ( not ns1 is empty implies not AND3 ((NOT1 nq3),(NOT1 nq2),nq1) is empty ) & ( not AND3 ((NOT1 nq3),(NOT1 nq2),nq1) is empty implies not ns1 is empty ) & ( not ns2 is empty implies not AND3 ((NOT1 nq3),nq2,(NOT1 nq1)) is empty ) & ( not AND3 ((NOT1 nq3),nq2,(NOT1 nq1)) is empty implies not ns2 is empty ) & ( not ns3 is empty implies not AND3 ((NOT1 nq3),nq2,nq1) is empty ) & ( not AND3 ((NOT1 nq3),nq2,nq1) is empty implies not ns3 is empty ) & ( not ns4 is empty implies not AND3 (nq3,(NOT1 nq2),(NOT1 nq1)) is empty ) & ( not AND3 (nq3,(NOT1 nq2),(NOT1 nq1)) is empty implies not ns4 is empty ) & ( not ns5 is empty implies not AND3 (nq3,(NOT1 nq2),nq1) is empty ) & ( not AND3 (nq3,(NOT1 nq2),nq1) is empty implies not ns5 is empty ) & ( not ns6 is empty implies not AND3 (nq3,nq2,(NOT1 nq1)) is empty ) & ( not AND3 (nq3,nq2,(NOT1 nq1)) is empty implies not ns6 is empty ) & ( not ns7 is empty implies not AND3 (nq3,nq2,nq1) is empty ) & ( not AND3 (nq3,nq2,nq1) is empty implies not ns7 is empty ) & ( not nq1 is empty implies not NOT1 q3 is empty ) & ( not NOT1 q3 is empty implies not nq1 is empty ) & ( not nq2 is empty implies not q1 is empty ) & ( not q1 is empty implies not nq2 is empty ) & ( not nq3 is empty implies not q2 is empty ) & ( not q2 is empty implies not nq3 is empty ) & not ( ( not ns1 is empty implies not s0 is empty ) & ( not s0 is empty implies not ns1 is empty ) & ( not ns3 is empty implies not s1 is empty ) & ( not s1 is empty implies not ns3 is empty ) & ( not ns7 is empty implies not s3 is empty ) & ( not s3 is empty implies not ns7 is empty ) & ( not ns6 is empty implies not s7 is empty ) & ( not s7 is empty implies not ns6 is empty ) & ( not ns4 is empty implies not s6 is empty ) & ( not s6 is empty implies not ns4 is empty ) & ( not ns0 is empty implies not s4 is empty ) & ( not s4 is empty implies not ns0 is empty ) & ( not ns2 is empty implies not s5 is empty ) & ( not s5 is empty implies not ns2 is empty ) & ( not ns5 is empty implies not s2 is empty ) & ( not s2 is empty implies not ns5 is empty ) ) )

assume that

A1: ( not s0 is empty iff not AND3 ((NOT1 q3),(NOT1 q2),(NOT1 q1)) is empty ) and

A2: ( not s1 is empty iff not AND3 ((NOT1 q3),(NOT1 q2),q1) is empty ) and

A3: ( not s2 is empty iff not AND3 ((NOT1 q3),q2,(NOT1 q1)) is empty ) and

A4: ( not s3 is empty iff not AND3 ((NOT1 q3),q2,q1) is empty ) and

A5: ( not s4 is empty iff not AND3 (q3,(NOT1 q2),(NOT1 q1)) is empty ) and

A6: ( not s5 is empty iff not AND3 (q3,(NOT1 q2),q1) is empty ) and

A7: ( not s6 is empty iff not AND3 (q3,q2,(NOT1 q1)) is empty ) and

A8: ( not s7 is empty iff not AND3 (q3,q2,q1) is empty ) and

A9: ( not ns0 is empty iff not AND3 ((NOT1 nq3),(NOT1 nq2),(NOT1 nq1)) is empty ) and

A10: ( not ns1 is empty iff not AND3 ((NOT1 nq3),(NOT1 nq2),nq1) is empty ) and

A11: ( not ns2 is empty iff not AND3 ((NOT1 nq3),nq2,(NOT1 nq1)) is empty ) and

A12: ( not ns3 is empty iff not AND3 ((NOT1 nq3),nq2,nq1) is empty ) and

A13: ( not ns4 is empty iff not AND3 (nq3,(NOT1 nq2),(NOT1 nq1)) is empty ) and

A14: ( not ns5 is empty iff not AND3 (nq3,(NOT1 nq2),nq1) is empty ) and

A15: ( not ns6 is empty iff not AND3 (nq3,nq2,(NOT1 nq1)) is empty ) and

A16: ( not ns7 is empty iff not AND3 (nq3,nq2,nq1) is empty ) and

A17: ( ( not nq1 is empty implies not NOT1 q3 is empty ) & ( not NOT1 q3 is empty implies not nq1 is empty ) & ( not nq2 is empty implies not q1 is empty ) & ( not q1 is empty implies not nq2 is empty ) & ( not nq3 is empty implies not q2 is empty ) & ( not q2 is empty implies not nq3 is empty ) ) ; :: thesis: ( ( not ns1 is empty implies not s0 is empty ) & ( not s0 is empty implies not ns1 is empty ) & ( not ns3 is empty implies not s1 is empty ) & ( not s1 is empty implies not ns3 is empty ) & ( not ns7 is empty implies not s3 is empty ) & ( not s3 is empty implies not ns7 is empty ) & ( not ns6 is empty implies not s7 is empty ) & ( not s7 is empty implies not ns6 is empty ) & ( not ns4 is empty implies not s6 is empty ) & ( not s6 is empty implies not ns4 is empty ) & ( not ns0 is empty implies not s4 is empty ) & ( not s4 is empty implies not ns0 is empty ) & ( not ns2 is empty implies not s5 is empty ) & ( not s5 is empty implies not ns2 is empty ) & ( not ns5 is empty implies not s2 is empty ) & ( not s2 is empty implies not ns5 is empty ) )

thus ( not ns1 is empty iff not s0 is empty ) by A1, A10, A17; :: thesis: ( ( not ns3 is empty implies not s1 is empty ) & ( not s1 is empty implies not ns3 is empty ) & ( not ns7 is empty implies not s3 is empty ) & ( not s3 is empty implies not ns7 is empty ) & ( not ns6 is empty implies not s7 is empty ) & ( not s7 is empty implies not ns6 is empty ) & ( not ns4 is empty implies not s6 is empty ) & ( not s6 is empty implies not ns4 is empty ) & ( not ns0 is empty implies not s4 is empty ) & ( not s4 is empty implies not ns0 is empty ) & ( not ns2 is empty implies not s5 is empty ) & ( not s5 is empty implies not ns2 is empty ) & ( not ns5 is empty implies not s2 is empty ) & ( not s2 is empty implies not ns5 is empty ) )

thus ( not ns3 is empty iff not s1 is empty ) by A2, A12, A17; :: thesis: ( ( not ns7 is empty implies not s3 is empty ) & ( not s3 is empty implies not ns7 is empty ) & ( not ns6 is empty implies not s7 is empty ) & ( not s7 is empty implies not ns6 is empty ) & ( not ns4 is empty implies not s6 is empty ) & ( not s6 is empty implies not ns4 is empty ) & ( not ns0 is empty implies not s4 is empty ) & ( not s4 is empty implies not ns0 is empty ) & ( not ns2 is empty implies not s5 is empty ) & ( not s5 is empty implies not ns2 is empty ) & ( not ns5 is empty implies not s2 is empty ) & ( not s2 is empty implies not ns5 is empty ) )

thus ( not ns7 is empty iff not s3 is empty ) by A4, A16, A17; :: thesis: ( ( not ns6 is empty implies not s7 is empty ) & ( not s7 is empty implies not ns6 is empty ) & ( not ns4 is empty implies not s6 is empty ) & ( not s6 is empty implies not ns4 is empty ) & ( not ns0 is empty implies not s4 is empty ) & ( not s4 is empty implies not ns0 is empty ) & ( not ns2 is empty implies not s5 is empty ) & ( not s5 is empty implies not ns2 is empty ) & ( not ns5 is empty implies not s2 is empty ) & ( not s2 is empty implies not ns5 is empty ) )

( not ns6 is empty iff ( not q3 is empty & not q2 is empty & not q1 is empty ) ) by A15, A17;

hence ( not ns6 is empty iff not s7 is empty ) by A8; :: thesis: ( ( not ns4 is empty implies not s6 is empty ) & ( not s6 is empty implies not ns4 is empty ) & ( not ns0 is empty implies not s4 is empty ) & ( not s4 is empty implies not ns0 is empty ) & ( not ns2 is empty implies not s5 is empty ) & ( not s5 is empty implies not ns2 is empty ) & ( not ns5 is empty implies not s2 is empty ) & ( not s2 is empty implies not ns5 is empty ) )

( not ns4 is empty iff ( not q3 is empty & not q2 is empty & not NOT1 q1 is empty ) ) by A13, A17;

hence ( not ns4 is empty iff not s6 is empty ) by A7; :: thesis: ( ( not ns0 is empty implies not s4 is empty ) & ( not s4 is empty implies not ns0 is empty ) & ( not ns2 is empty implies not s5 is empty ) & ( not s5 is empty implies not ns2 is empty ) & ( not ns5 is empty implies not s2 is empty ) & ( not s2 is empty implies not ns5 is empty ) )

( not ns0 is empty iff ( not q3 is empty & not NOT1 q2 is empty & not NOT1 q1 is empty ) ) by A9, A17;

hence ( not ns0 is empty iff not s4 is empty ) by A5; :: thesis: ( ( not ns2 is empty implies not s5 is empty ) & ( not s5 is empty implies not ns2 is empty ) & ( not ns5 is empty implies not s2 is empty ) & ( not s2 is empty implies not ns5 is empty ) )

( not ns2 is empty iff ( not q3 is empty & not NOT1 q2 is empty & not q1 is empty ) ) by A11, A17;

hence ( not ns2 is empty iff not s5 is empty ) by A6; :: thesis: ( not ns5 is empty iff not s2 is empty )

thus ( not ns5 is empty iff not s2 is empty ) by A3, A14, A17; :: thesis: verum

assume that

A1: ( not s0 is empty iff not AND3 ((NOT1 q3),(NOT1 q2),(NOT1 q1)) is empty ) and

A2: ( not s1 is empty iff not AND3 ((NOT1 q3),(NOT1 q2),q1) is empty ) and

A3: ( not s2 is empty iff not AND3 ((NOT1 q3),q2,(NOT1 q1)) is empty ) and

A4: ( not s3 is empty iff not AND3 ((NOT1 q3),q2,q1) is empty ) and

A5: ( not s4 is empty iff not AND3 (q3,(NOT1 q2),(NOT1 q1)) is empty ) and

A6: ( not s5 is empty iff not AND3 (q3,(NOT1 q2),q1) is empty ) and

A7: ( not s6 is empty iff not AND3 (q3,q2,(NOT1 q1)) is empty ) and

A8: ( not s7 is empty iff not AND3 (q3,q2,q1) is empty ) and

A9: ( not ns0 is empty iff not AND3 ((NOT1 nq3),(NOT1 nq2),(NOT1 nq1)) is empty ) and

A10: ( not ns1 is empty iff not AND3 ((NOT1 nq3),(NOT1 nq2),nq1) is empty ) and

A11: ( not ns2 is empty iff not AND3 ((NOT1 nq3),nq2,(NOT1 nq1)) is empty ) and

A12: ( not ns3 is empty iff not AND3 ((NOT1 nq3),nq2,nq1) is empty ) and

A13: ( not ns4 is empty iff not AND3 (nq3,(NOT1 nq2),(NOT1 nq1)) is empty ) and

A14: ( not ns5 is empty iff not AND3 (nq3,(NOT1 nq2),nq1) is empty ) and

A15: ( not ns6 is empty iff not AND3 (nq3,nq2,(NOT1 nq1)) is empty ) and

A16: ( not ns7 is empty iff not AND3 (nq3,nq2,nq1) is empty ) and

A17: ( ( not nq1 is empty implies not NOT1 q3 is empty ) & ( not NOT1 q3 is empty implies not nq1 is empty ) & ( not nq2 is empty implies not q1 is empty ) & ( not q1 is empty implies not nq2 is empty ) & ( not nq3 is empty implies not q2 is empty ) & ( not q2 is empty implies not nq3 is empty ) ) ; :: thesis: ( ( not ns1 is empty implies not s0 is empty ) & ( not s0 is empty implies not ns1 is empty ) & ( not ns3 is empty implies not s1 is empty ) & ( not s1 is empty implies not ns3 is empty ) & ( not ns7 is empty implies not s3 is empty ) & ( not s3 is empty implies not ns7 is empty ) & ( not ns6 is empty implies not s7 is empty ) & ( not s7 is empty implies not ns6 is empty ) & ( not ns4 is empty implies not s6 is empty ) & ( not s6 is empty implies not ns4 is empty ) & ( not ns0 is empty implies not s4 is empty ) & ( not s4 is empty implies not ns0 is empty ) & ( not ns2 is empty implies not s5 is empty ) & ( not s5 is empty implies not ns2 is empty ) & ( not ns5 is empty implies not s2 is empty ) & ( not s2 is empty implies not ns5 is empty ) )

thus ( not ns1 is empty iff not s0 is empty ) by A1, A10, A17; :: thesis: ( ( not ns3 is empty implies not s1 is empty ) & ( not s1 is empty implies not ns3 is empty ) & ( not ns7 is empty implies not s3 is empty ) & ( not s3 is empty implies not ns7 is empty ) & ( not ns6 is empty implies not s7 is empty ) & ( not s7 is empty implies not ns6 is empty ) & ( not ns4 is empty implies not s6 is empty ) & ( not s6 is empty implies not ns4 is empty ) & ( not ns0 is empty implies not s4 is empty ) & ( not s4 is empty implies not ns0 is empty ) & ( not ns2 is empty implies not s5 is empty ) & ( not s5 is empty implies not ns2 is empty ) & ( not ns5 is empty implies not s2 is empty ) & ( not s2 is empty implies not ns5 is empty ) )

thus ( not ns3 is empty iff not s1 is empty ) by A2, A12, A17; :: thesis: ( ( not ns7 is empty implies not s3 is empty ) & ( not s3 is empty implies not ns7 is empty ) & ( not ns6 is empty implies not s7 is empty ) & ( not s7 is empty implies not ns6 is empty ) & ( not ns4 is empty implies not s6 is empty ) & ( not s6 is empty implies not ns4 is empty ) & ( not ns0 is empty implies not s4 is empty ) & ( not s4 is empty implies not ns0 is empty ) & ( not ns2 is empty implies not s5 is empty ) & ( not s5 is empty implies not ns2 is empty ) & ( not ns5 is empty implies not s2 is empty ) & ( not s2 is empty implies not ns5 is empty ) )

thus ( not ns7 is empty iff not s3 is empty ) by A4, A16, A17; :: thesis: ( ( not ns6 is empty implies not s7 is empty ) & ( not s7 is empty implies not ns6 is empty ) & ( not ns4 is empty implies not s6 is empty ) & ( not s6 is empty implies not ns4 is empty ) & ( not ns0 is empty implies not s4 is empty ) & ( not s4 is empty implies not ns0 is empty ) & ( not ns2 is empty implies not s5 is empty ) & ( not s5 is empty implies not ns2 is empty ) & ( not ns5 is empty implies not s2 is empty ) & ( not s2 is empty implies not ns5 is empty ) )

( not ns6 is empty iff ( not q3 is empty & not q2 is empty & not q1 is empty ) ) by A15, A17;

hence ( not ns6 is empty iff not s7 is empty ) by A8; :: thesis: ( ( not ns4 is empty implies not s6 is empty ) & ( not s6 is empty implies not ns4 is empty ) & ( not ns0 is empty implies not s4 is empty ) & ( not s4 is empty implies not ns0 is empty ) & ( not ns2 is empty implies not s5 is empty ) & ( not s5 is empty implies not ns2 is empty ) & ( not ns5 is empty implies not s2 is empty ) & ( not s2 is empty implies not ns5 is empty ) )

( not ns4 is empty iff ( not q3 is empty & not q2 is empty & not NOT1 q1 is empty ) ) by A13, A17;

hence ( not ns4 is empty iff not s6 is empty ) by A7; :: thesis: ( ( not ns0 is empty implies not s4 is empty ) & ( not s4 is empty implies not ns0 is empty ) & ( not ns2 is empty implies not s5 is empty ) & ( not s5 is empty implies not ns2 is empty ) & ( not ns5 is empty implies not s2 is empty ) & ( not s2 is empty implies not ns5 is empty ) )

( not ns0 is empty iff ( not q3 is empty & not NOT1 q2 is empty & not NOT1 q1 is empty ) ) by A9, A17;

hence ( not ns0 is empty iff not s4 is empty ) by A5; :: thesis: ( ( not ns2 is empty implies not s5 is empty ) & ( not s5 is empty implies not ns2 is empty ) & ( not ns5 is empty implies not s2 is empty ) & ( not s2 is empty implies not ns5 is empty ) )

( not ns2 is empty iff ( not q3 is empty & not NOT1 q2 is empty & not q1 is empty ) ) by A11, A17;

hence ( not ns2 is empty iff not s5 is empty ) by A6; :: thesis: ( not ns5 is empty iff not s2 is empty )

thus ( not ns5 is empty iff not s2 is empty ) by A3, A14, A17; :: thesis: verum