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

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