hereby :: thesis: ( ( for x being Element of dom GF holds GF . x is chordal ) implies GF is chordal )

assume A1: GF is chordal ; :: thesis: for x being Element of dom GF holds GF . x is chordal
let x be Element of dom GF; :: thesis: GF . x is chordal
ex G being _Graph st
( GF . x = G & G is chordal ) by A1;
hence GF . x is chordal ; :: thesis: verum

end;

assume A3: for x being Element of dom GF holds GF . x is chordal ; :: thesis: GF is chordal
let x be object ; :: according to GLIBPRE0:def 4 :: thesis: ( x in dom GF implies ex G being _Graph st
( GF . x = G & G is chordal ) )
assume x in dom GF ; :: thesis: ex G being _Graph st
( GF . x = G & G is chordal )
then reconsider y = x as Element of dom GF ;
take GF . y ; :: thesis: ( GF . x = GF . y & GF . y is chordal )
thus ( GF . x = GF . y & GF . y is chordal ) by A3; :: thesis: verum