take G_Real ; :: thesis: ( G_Real is strict & G_Real is add-associative & G_Real is right_zeroed & G_Real is right_complementable & G_Real is Abelian )
thus ( G_Real is strict & G_Real is add-associative & G_Real is right_zeroed & G_Real is right_complementable & G_Real is Abelian ) ; :: thesis: verum