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;
A4: 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 ;
A5: 0 <= y by A1, A4, SIN_COS6:85, XXREAL_1:1;
A6: y <= PI by A1, A4, SIN_COS6:85, XXREAL_1:1;
reconsider x = x as Real by A2;
A7: - 1 < x by A2, Lm55, XXREAL_1:2;
A8: x <= 1 by A2, Lm55, XXREAL_1:2;
y = arccos . x by A2, A3, Lm55, FUNCT_1:49
.= arccos x by SIN_COS6:def 4 ;
then y < PI by A6, A7, A8, SIN_COS6:98, XXREAL_0:1;
hence y in E by A5, XXREAL_1:3; :: thesis: verum