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

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

end;

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