let ET be non empty strict U_FMT_filter FMT_Space_Str ; :: thesis: for x being Element of ET holds the carrier of ET in U_FMT x
let x be Element of ET; :: thesis: the carrier of ET in U_FMT x
U_FMT x is Filter of the carrier of ET by Def2;
hence the carrier of ET in U_FMT x by CARD_FIL:5; :: thesis: verum