set R = a -reflection ;
(a -reflection) * (a -reflection) = id E by Th17;
hence ( a -reflection is one-to-one & a -reflection is onto ) by FUNCT_2:23; :: according to FUNCT_2:def 4 :: thesis: verum