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;
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