Bottom L is_a_unity_wrt the L_join of L by Th51;
hence the L_join of L is having_a_unity ; :: thesis: verum