take Top L ; :: thesis: Top L is irreducible
thus Top L is irreducible by Th10; :: thesis: verum