{ D where D is Subset of REAL : ex r being real number st D = halfline r } is Subset-Family of REAL

proof

now

let p be set ; :: thesis: ( p in { D where D is Subset of REAL : ex r being real number st D = halfline r } implies p in bool REAL )
assume p in { D where D is Subset of REAL : ex r being real number st D = halfline r } ; :: thesis: p in bool REAL
then ex D being Subset of REAL st
( p = D & ex r being real number st D = halfline r ) ;
hence p in bool REAL ; :: thesis: verum

end;

hence { D where D is Subset of REAL : ex r being real number st D = halfline r } is Subset-Family of REAL by TARSKI:def 3; :: thesis: verum

end;

hence { D where D is Subset of REAL : ex r being real number st D = halfline r } is Subset-Family of REAL ; :: thesis: verum