let M be non empty right_unital multLoopStr ; :: thesis: for ell being Element of M holds
( ell is unital iff ell in units M )
let ell be Element of M; :: thesis: ( ell is unital iff ell in units M )
thus ( ell is unital implies ell in units M ) ; :: thesis: ( ell in units M implies ell is unital )
assume ell in units M ; :: thesis: ell is unital
then consider x being Element of M such that
A1: ( ell = x & x is unital ) ;
thus ell is unital by A1; :: thesis: verum