[.((3 / 4) * PI),PI.] c= ].(PI / 2),PI.] by Lm6, XXREAL_2:def 12;
hence dom (sec | [.((3 / 4) * PI),PI.]) = [.((3 / 4) * PI),PI.] by Th2, RELAT_1:62, XBOOLE_1:1; :: thesis: verum