{ [.-infty,r.] where r is Real : verum } c= bool ExtREAL

proof

hence
{ [.-infty,r.] where r is Real : verum } is Subset-Family of ExtREAL
; :: thesis: verum
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;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