For proving [Graphics:submitted.nbgr199.gif], by [Graphics:submitted.nbgr200.gif], it suffices to prove

[Graphics:submitted.nbgr201.gif] [Graphics:submitted.nbgr202.gif].

We prove the individual conjunctive parts of [Graphics:submitted.nbgr203.gif]:

Proof of [Graphics:submitted.nbgr204.gif] [Graphics:submitted.nbgr205.gif]:

Formula [Graphics:submitted.nbgr206.gif] is simplified to

[Graphics:submitted.nbgr207.gif] [Graphics:submitted.nbgr208.gif].

For proving [Graphics:submitted.nbgr209.gif], by [Graphics:submitted.nbgr210.gif], it suffices to prove

[Graphics:submitted.nbgr211.gif] [Graphics:submitted.nbgr212.gif].

From [Graphics:submitted.nbgr213.gif] by specialization we obtain

[Graphics:submitted.nbgr214.gif] [Graphics:submitted.nbgr215.gif].

From [Graphics:submitted.nbgr216.gif] by specialization we obtain

[Graphics:submitted.nbgr217.gif] [Graphics:submitted.nbgr218.gif].

We prove first

[Graphics:submitted.nbgr219.gif] [Graphics:submitted.nbgr220.gif].

We prove the individual conjunctive parts of [Graphics:submitted.nbgr230.gif]:

From [Graphics:submitted.nbgr248.gif] and [Graphics:submitted.nbgr249.gif] we obtain by modus ponens

Proof of [Graphics:submitted.nbgr250.gif] [Graphics:submitted.nbgr251.gif]:

Formula [Graphics:submitted.nbgr252.gif] is true because it is identical to [Graphics:submitted.nbgr253.gif].