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

(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