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