{ (halfline r) where r is Element of REAL : verum } c= bool REAL

proof

hence
{ (halfline r) where r is Element of REAL : verum } is Subset-Family of REAL
; :: thesis: verum
let p be object ; :: according to TARSKI:def 3 :: thesis: ( not p in { (halfline r) where r is Element of REAL : verum } or p in bool REAL )

assume p in { (halfline r) where r is Element of REAL : verum } ; :: thesis: p in bool REAL

then ex r being Element of REAL st p = halfline r ;

hence p in bool REAL ; :: thesis: verum

end;assume p in { (halfline r) where r is Element of REAL : verum } ; :: thesis: p in bool REAL

then ex r being Element of REAL st p = halfline r ;

hence p in bool REAL ; :: thesis: verum