let X be non empty set ; :: thesis: for F being BinOp of X holds
( F is having_a_unity iff the_unity_wrt F is_a_unity_wrt F )
let F be BinOp of X; :: thesis: ( F is having_a_unity iff the_unity_wrt F is_a_unity_wrt F )
thus ( F is having_a_unity implies the_unity_wrt F is_a_unity_wrt F ) :: thesis: ( the_unity_wrt F is_a_unity_wrt F implies F is having_a_unity )

proof

assume F is having_a_unity ; :: thesis: the_unity_wrt F is_a_unity_wrt F
then ex x being Element of X st x is_a_unity_wrt F by Def2;
hence the_unity_wrt F is_a_unity_wrt F by BINOP_1:def 8; :: thesis: verum

end;

thus ( the_unity_wrt F is_a_unity_wrt F implies F is having_a_unity ) by Def2; :: thesis: verum