[.(PI / 4),(PI / 2).] c= ].0,(PI / 2).] by Lm8, XXREAL_2:def 12;
hence dom (cosec | [.(PI / 4),(PI / 2).]) = [.(PI / 4),(PI / 2).] by Th4, RELAT_1:62, XBOOLE_1:1; :: thesis: verum