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

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