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