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