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 Th37;
hence A ^Fodelta = (A ^Fob) /\ ((A ^Foi) `) by Th39; :: thesis: verum