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