let p be Element of GRZ-symbols ; :: thesis: ( p . 1 = 0 iff p in VAR )
thus ( p . 1 = 0 implies p in VAR ) :: thesis: ( p in VAR implies p . 1 = 0 )

proof

assume p . 1 = 0 ; :: thesis: p in VAR
then not p in GRZ-ops by Lm2;
hence p in VAR by XBOOLE_0:def 3; :: thesis: verum

end;

thus ( p in VAR implies p . 1 = 0 ) by Lm1; :: thesis: verum