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 A1: G1 is Subgraph of G ;
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 A2: x in the carrier' of G1 and
A3: the Source of G1 . x = the Target of G1 . x ; :: thesis: contradiction
A4: the carrier' of G1 c= the carrier' of G by A1, Def18;
the Source of G . x = the Target of G1 . x by A1, A2, A3, Def18
.= the Target of G . x by A1, A2, Def18 ;
hence contradiction by A2, A4, Def9; :: thesis: verum

end;

hence G1 is simple ; :: thesis: verum