take F ; :: thesis: F = uparrow (fininfs F)
thus F = uparrow (fininfs F) by Lm3; :: thesis: verum