let x be Element of REAL+ ; :: thesis: GLUED (DEDEKIND_CUT x) = x
DEDEKIND_CUT (GLUED (DEDEKIND_CUT x)) = DEDEKIND_CUT x by Lm12;
hence GLUED (DEDEKIND_CUT x) = x by Lm22; :: thesis: verum