{ (right_closed_halfline r) where r is Element of REAL : verum } c= bool REAL
proof
let p be object ; :: according to TARSKI:def 3 :: thesis: ( not p in { (right_closed_halfline r) where r is Element of REAL : verum } or p in bool REAL )
assume p in { (right_closed_halfline r) where r is Element of REAL : verum } ; :: thesis: p in bool REAL
then ex r being Element of REAL st p = right_closed_halfline r ;
hence p in bool REAL ; :: thesis: verum
end;
hence { (right_closed_halfline r) where r is Element of REAL : verum } is Subset-Family of REAL ; :: thesis: verum