consider a being Element of R such that
A1: ( a <> 1. R & a <> 0. R ) by Def1;
take a ; :: thesis: not a is trivial
thus not a is trivial by A1; :: thesis: verum