set SF = { (fundamental_element_of_entourages (MS,r)) where r is positive Real : verum } ;
{ (fundamental_element_of_entourages (MS,r)) where r is positive Real : verum } c= bool [: the carrier of MS, the carrier of MS:]

proof

let t be object ; :: according to TARSKI:def 3 :: thesis: ( not t in { (fundamental_element_of_entourages (MS,r)) where r is positive Real : verum } or t in bool [: the carrier of MS, the carrier of MS:] )
assume t in { (fundamental_element_of_entourages (MS,r)) where r is positive Real : verum } ; :: thesis: t in bool [: the carrier of MS, the carrier of MS:]
then consider r being positive Real such that
A1: t = fundamental_element_of_entourages (MS,r) ;
reconsider t1 = t as Subset of [: the carrier of MS, the carrier of MS:] by A1;
t1 c= [: the carrier of MS, the carrier of MS:] ;
hence t in bool [: the carrier of MS, the carrier of MS:] ; :: thesis: verum

end;

then reconsider SF = { (fundamental_element_of_entourages (MS,r)) where r is positive Real : verum } as Subset-Family of [: the carrier of MS, the carrier of MS:] ;
fundamental_element_of_entourages (MS,1) in SF ;
hence { (fundamental_element_of_entourages (MS,r)) where r is positive Real : verum } is non empty Subset-Family of [: the carrier of MS, the carrier of MS:] ; :: thesis: verum