let A be non empty Subset of GRZ-formula-set; for t, u being GRZ-formula holds
( A, GRZ-rules |- t '&' u iff ( A, GRZ-rules |- t & A, GRZ-rules |- u ) )
let t, u be GRZ-formula; ( A, GRZ-rules |- t '&' u iff ( A, GRZ-rules |- t & A, GRZ-rules |- u ) )
thus
( A, GRZ-rules |- t '&' u implies ( A, GRZ-rules |- t & A, GRZ-rules |- u ) )
( A, GRZ-rules |- t & A, GRZ-rules |- u implies A, GRZ-rules |- t '&' u )proof
assume A1:
A,
GRZ-rules |- t '&' u
;
( A, GRZ-rules |- t & A, GRZ-rules |- u )
set S =
{(t '&' u)};
for
a being
object st
a in {(t '&' u)} holds
a in GRZ-formula-set
then
{(t '&' u)} c= GRZ-formula-set
;
then reconsider S =
{(t '&' u)} as
GRZ-formula-finset ;
A2:
A,
GRZ-rules |- S
by A1, TARSKI:def 1;
[S,t] in GRZ-ConjElimL
;
then
[S,t] in GRZ-rules
by Def35;
hence
A,
GRZ-rules |- t
by A2, Th48;
A, GRZ-rules |- u
[S,u] in GRZ-ConjElimR
;
then
[S,u] in GRZ-rules
by Def35;
hence
A,
GRZ-rules |- u
by A2, Th48;
verum
end;
assume that
A10:
A, GRZ-rules |- t
and
A11:
A, GRZ-rules |- u
; A, GRZ-rules |- t '&' u
set S1 = {t,u};
for a being object st a in {t,u} holds
a in GRZ-formula-set
then
{t,u} c= GRZ-formula-set
;
then reconsider S1 = {t,u} as GRZ-formula-finset ;
A12:
A, GRZ-rules |- S1
by A10, A11, TARSKI:def 2;
[S1,(t '&' u)] in GRZ-ConjIntro
;
then
[S1,(t '&' u)] in GRZ-rules
by Def35;
hence
A, GRZ-rules |- t '&' u
by A12, Th48; verum