let FMT be non empty FMT_Space_Str ; :: thesis: for A being Subset of FMT holds A ^Fodelta = (A ^Fob) /\ ((A ^Foi) `)
let A be Subset of FMT; :: thesis: A ^Fodelta = (A ^Fob) /\ ((A ^Foi) `)
((A `) ^Fob) ` = A ^Foi by Th38;
hence A ^Fodelta = (A ^Fob) /\ ((A ^Foi) `) by Th40; :: thesis: verum