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