let FT be non empty filled RelStr ; :: thesis: { (U_FT x) where x is Element of : verum } is Cover of
let a be set ; :: according to TARSKI:def 3,SETFAM_1:def 12 :: thesis: ( not a in the carrier of FT or a in union { (U_FT x) where x is Element of : verum } )
assume a in the carrier of FT ; :: thesis: a in union { (U_FT x) where x is Element of : verum }
then reconsider b = a as Element of ;
( b in U_FT b & U_FT b in { (U_FT x) where x is Element of : verum } ) by Def4;
hence a in union { (U_FT x) where x is Element of : verum } by TARSKI:def 4; :: thesis: verum