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