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