theorem :: COMPLEX1:30

1r *' = 1r by Th6;