let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in rng (ac | (R^1 Q)) or y in E )
assume A1: y in rng (ac | (R^1 Q)) ; :: thesis: y in E
then consider x being set such that
A2: x in dom (ac | (R^1 Q)) and
A3: (ac | (R^1 Q)) . x = y by FUNCT_1:def 5;
reconsider x = x as Real by A2, Lm38;
A4: rng (ac | (R^1 Q)) c= rng ac by RELAT_1:99;
then y in [.0 ,PI .] by A1, SIN_COS6:87;
then reconsider y = y as Real ;
A5: ( 0 <= y & y <= PI ) by A1, A4, SIN_COS6:87, XXREAL_1:1;
A6: ( - 1 <= x & x < 1 ) by A2, Lm38, XXREAL_1:3;
y = arccos . x by A2, A3, Lm38, FUNCT_1:72
.= arccos x by SIN_COS6:def 4 ;
then y <> 0 by A6, SIN_COS6:98;
hence y in E by A5, XXREAL_1:2; :: thesis: verum