hereby :: thesis: ( ( for n being Nat holds GSq . n is edgeless ) implies GSq is edgeless )

assume A1: GSq is edgeless ; :: thesis: for x being Nat holds GSq . x is edgeless
let x be Nat; :: thesis: GSq . x is edgeless
x in dom GSq by Lm10;
hence GSq . x is edgeless by A1; :: thesis: verum

end;

assume A2: for x being Nat holds GSq . x is edgeless ; :: thesis: GSq is edgeless
let x be Element of dom GSq; :: according to GLIB_008:def 3 :: thesis: GSq . x is edgeless
thus GSq . x is edgeless by A2; :: thesis: verum