hereby :: thesis: ( ( for x being Nat holds not GSq . x is trivial ) implies GSq is non-trivial )

assume A1: GSq is non-trivial ; :: thesis: for x being Nat holds not GSq . x is trivial
let x be Nat; :: thesis: not GSq . x is trivial
x in dom GSq by LmNat;
then x is Element of dom GSq ;
hence not GSq . x is trivial by A1; :: thesis: verum

end;

assume A2: for x being Nat holds not GSq . x is trivial ; :: thesis: GSq is non-trivial
let x be Element of dom GSq; :: according to GLIB_000:def 69 :: thesis: not GSq . x is trivial
thus not GSq . x is trivial by A2; :: thesis: verum