let G1 be Graph; :: thesis: for G being simple Graph st G1 c= G holds
G1 is simple
let G be simple Graph; :: thesis: ( G1 c= G implies G1 is simple )
assume A1: G1 c= G ; :: thesis: G1 is simple
A2: G1 is Subgraph of G by A1, Def24;
A3: for x being set holds
( not x in the carrier' of G1 or not the Source of G1 . x = the Target of G1 . x )

proof

given x being set such that A4: x in the carrier' of G1 and
A5: the Source of G1 . x = the Target of G1 . x ; :: thesis: contradiction
A6: the carrier' of G1 c= the carrier' of G by A2, Def18;
A7: the Source of G . x = the Target of G1 . x by A2, A4, A5, Def18
.= the Target of G . x by A2, A4, Def18 ;
thus contradiction by A4, A6, A7, Def7; :: thesis: verum

end;

thus G1 is simple by A3, Def7; :: thesis: verum