let r be Element of T; :: thesis: r is finite
@ r = r ;
hence r is finite ; :: thesis: verum