let k1, k2 be Real; :: thesis: ].k1,k2.] is Event of Borel_Sets
A1: [.k1,k2.] is Element of Borel_Sets by FINANCE1:8;
A2: {k1} is Event of Borel_Sets by Th1;
reconsider k1 = k1, k2 = k2 as ExtReal ;

per cases ( k1 <= k2 or k1 > k2 ) ;

suppose B1: k1 <= k2 ; :: thesis: ].k1,k2.] is Event of Borel_Sets

[.k1,k2.] \ {k1} is Element of Borel_Sets by A1, A2, PROB_1:24;
hence ].k1,k2.] is Event of Borel_Sets by B1, XXREAL_1:134; :: thesis: verum

end;

suppose k1 > k2 ; :: thesis: ].k1,k2.] is Event of Borel_Sets

then ].k1,k2.] = {} by XXREAL_1:26;
hence ].k1,k2.] is Event of Borel_Sets by PROB_1:4; :: thesis: verum

end;

end;