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 G1 c= G ; :: thesis: G1 is simple
then A2: G1 is Subgraph of G by Def24;
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;
the Source of G . x = the Target of G1 . x by A2, A4, A5, Def18
.= the Target of G . x by A2, A4, Def18 ;
hence contradiction by A4, A6, Def7; :: thesis: verum

end;

hence G1 is simple by Def7; :: thesis: verum