let s0, s1, s2, s3, ns0, ns1, ns2, ns3, q1, q2, nq1, nq2 be set ; not ( ( not s0 is empty implies not AND2 ((NOT1 q2),(NOT1 q1)) is empty ) & ( not AND2 ((NOT1 q2),(NOT1 q1)) is empty implies not s0 is empty ) & ( not s1 is empty implies not AND2 ((NOT1 q2),q1) is empty ) & ( not AND2 ((NOT1 q2),q1) is empty implies not s1 is empty ) & ( not s2 is empty implies not AND2 (q2,(NOT1 q1)) is empty ) & ( not AND2 (q2,(NOT1 q1)) is empty implies not s2 is empty ) & ( not s3 is empty implies not AND2 (q2,q1) is empty ) & ( not AND2 (q2,q1) is empty implies not s3 is empty ) & ( not ns0 is empty implies not AND2 ((NOT1 nq2),(NOT1 nq1)) is empty ) & ( not AND2 ((NOT1 nq2),(NOT1 nq1)) is empty implies not ns0 is empty ) & ( not ns1 is empty implies not AND2 ((NOT1 nq2),nq1) is empty ) & ( not AND2 ((NOT1 nq2),nq1) is empty implies not ns1 is empty ) & ( not ns2 is empty implies not AND2 (nq2,(NOT1 nq1)) is empty ) & ( not AND2 (nq2,(NOT1 nq1)) is empty implies not ns2 is empty ) & ( not ns3 is empty implies not AND2 (nq2,nq1) is empty ) & ( not AND2 (nq2,nq1) is empty implies not ns3 is empty ) & ( not nq1 is empty implies not NOT1 q2 is empty ) & ( not NOT1 q2 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 ( ( 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 ns2 is empty implies not s3 is empty ) & ( not s3 is empty implies not ns2 is empty ) & ( not ns0 is empty implies not s2 is empty ) & ( not s2 is empty implies not ns0 is empty ) ) )
assume that
A1:
( not s0 is empty iff not AND2 ((NOT1 q2),(NOT1 q1)) is empty )
and
A2:
( not s1 is empty iff not AND2 ((NOT1 q2),q1) is empty )
and
A3:
( not s2 is empty iff not AND2 (q2,(NOT1 q1)) is empty )
and
A4:
( not s3 is empty iff not AND2 (q2,q1) is empty )
and
A5:
( not ns0 is empty iff not AND2 ((NOT1 nq2),(NOT1 nq1)) is empty )
and
A6:
( not ns1 is empty iff not AND2 ((NOT1 nq2),nq1) is empty )
and
A7:
( not ns2 is empty iff not AND2 (nq2,(NOT1 nq1)) is empty )
and
A8:
( not ns3 is empty iff not AND2 (nq2,nq1) is empty )
and
A9:
( ( not nq1 is empty implies not NOT1 q2 is empty ) & ( not NOT1 q2 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 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 ns2 is empty implies not s3 is empty ) & ( not s3 is empty implies not ns2 is empty ) & ( not ns0 is empty implies not s2 is empty ) & ( not s2 is empty implies not ns0 is empty ) )
thus
( not ns1 is empty iff not s0 is empty )
by A1, A6, A9; ( ( not ns3 is empty implies not s1 is empty ) & ( not s1 is empty implies not ns3 is empty ) & ( not ns2 is empty implies not s3 is empty ) & ( not s3 is empty implies not ns2 is empty ) & ( not ns0 is empty implies not s2 is empty ) & ( not s2 is empty implies not ns0 is empty ) )
thus
( not ns3 is empty iff not s1 is empty )
by A2, A8, A9; ( ( not ns2 is empty implies not s3 is empty ) & ( not s3 is empty implies not ns2 is empty ) & ( not ns0 is empty implies not s2 is empty ) & ( not s2 is empty implies not ns0 is empty ) )
( not ns2 is empty iff ( not q2 is empty & not q1 is empty ) )
by A7, A9;
hence
( not ns2 is empty iff not s3 is empty )
by A4; ( not ns0 is empty iff not s2 is empty )
( not ns0 is empty iff ( not q2 is empty & not NOT1 q1 is empty ) )
by A5, A9;
hence
( not ns0 is empty iff not s2 is empty )
by A3; verum