take F ; :: thesis: F is F -extending
thus F is F -extending by Th1; :: thesis: verum