{ [.-infty,r.] where r is Real : verum } c= bool ExtREAL
proof
let p be object ; :: according to TARSKI:def 3 :: thesis: ( not p in { [.-infty,r.] where r is Real : verum } or p in bool ExtREAL )
assume p in { [.-infty,r.] where r is Real : verum } ; :: thesis: p in bool ExtREAL
then consider r being Real such that
A1: p = [.-infty,r.] ;
reconsider pp = p as set by A1;
pp c= ExtREAL by A1, MEMBERED:2;
hence p in bool ExtREAL ; :: thesis: verum
end;
hence { [.-infty,r.] where r is Real : verum } is Subset-Family of ExtREAL ; :: thesis: verum