take Top L ; :: thesis: Top L is prime
thus Top L is prime by Th20; :: thesis: verum