let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Family_of_halflines or x in Ext_Borel_Sets )
assume x in Family_of_halflines ; :: thesis: x in Ext_Borel_Sets
then consider r being Element of REAL such that
A1: x = halfline r ;
reconsider Set1 = [.-infty,r.] as Element of Ext_Borel_Sets by Th3;
reconsider Set2 = {r} as Element of Ext_Borel_Sets by Th71;
reconsider Set3 = Set1 \ Set2 as Element of Ext_Borel_Sets ;
A3: Set3 = [.-infty,r.[ by XXREAL_1:135, XXREAL_0:5;
reconsider Set4 = {-infty} as Element of Ext_Borel_Sets by Th500, Th600;
reconsider Set5 = Set3 \ Set4 as Element of Ext_Borel_Sets ;
Set5 = ].-infty,r.[ by XXREAL_1:136, A3, XXREAL_0:12;
hence x in Ext_Borel_Sets by A1; :: thesis: verum