Top L is_a_unity_wrt the L_meet of L by Th56;
hence the L_meet of L is having_a_unity ; :: thesis: verum