let G1 be Graph; for G being non-multi Graph st G1 c= G holds
G1 is non-multi
let G be non-multi Graph; ( G1 c= G implies G1 is non-multi )
assume
G1 c= G
; G1 is non-multi
then A1:
G1 is Subgraph of G
;
for x, y being set st x in the carrier' of G1 & y in the carrier' of G1 & ( ( the Source of G1 . x = the Source of G1 . y & the Target of G1 . x = the Target of G1 . y ) or ( the Source of G1 . x = the Target of G1 . y & the Source of G1 . y = the Target of G1 . x ) ) holds
x = y
proof
let x,
y be
set ;
( x in the carrier' of G1 & y in the carrier' of G1 & ( ( the Source of G1 . x = the Source of G1 . y & the Target of G1 . x = the Target of G1 . y ) or ( the Source of G1 . x = the Target of G1 . y & the Source of G1 . y = the Target of G1 . x ) ) implies x = y )
assume A2:
(
x in the
carrier' of
G1 &
y in the
carrier' of
G1 )
;
( ( not ( the Source of G1 . x = the Source of G1 . y & the Target of G1 . x = the Target of G1 . y ) & not ( the Source of G1 . x = the Target of G1 . y & the Source of G1 . y = the Target of G1 . x ) ) or x = y )
assume A3:
( ( the
Source of
G1 . x = the
Source of
G1 . y & the
Target of
G1 . x = the
Target of
G1 . y ) or ( the
Source of
G1 . x = the
Target of
G1 . y & the
Source of
G1 . y = the
Target of
G1 . x ) )
;
x = y
A4:
the
carrier' of
G1 c= the
carrier' of
G
by A1, Def18;
A5:
( the
Source of
G1 . x = the
Source of
G . x & the
Source of
G1 . y = the
Source of
G . y )
by A1, A2, Def18;
( the
Target of
G1 . x = the
Target of
G . x & the
Target of
G1 . y = the
Target of
G . y )
by A1, A2, Def18;
hence
x = y
by A2, A3, A4, A5, Def8;
verum
end;
hence
G1 is non-multi
; verum