let y be object ; :: 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 object such that
A2: x in dom (ac | (R^1 Q)) and
A3: (ac | (R^1 Q)) . x = y by FUNCT_1:def 3;
reconsider x = x as Real by A2;
A4: - 1 <= x by A2, Lm36, XXREAL_1:3;
A5: x < 1 by A2, Lm36, XXREAL_1:3;
A6: rng (ac | (R^1 Q)) c= rng ac by RELAT_1:70;
then y in [.0,PI.] by A1, SIN_COS6:85;
then reconsider y = y as Real ;
A7: y <= PI by A1, A6, SIN_COS6:85, XXREAL_1:1;
y = arccos . x by A2, A3, Lm36, FUNCT_1:49
.= arccos x by SIN_COS6:def 4 ;
then A8: y <> 0 by A4, A5, SIN_COS6:96;
0 <= y by A1, A6, SIN_COS6:85, XXREAL_1:1;
hence y in E by A7, A8, XXREAL_1:2; :: thesis: verum