set X = G_Real ;
not G_Real is trivial by TDGROUP:6;
hence ex b₁ being Uniquely_Two_Divisible_Group st
( b₁ is strict & not b₁ is trivial ) ; :: thesis: verum