let G1 be Graph; for G being oriented Graph st G1 c= G holds
G1 is oriented
let G be oriented Graph; ( G1 c= G implies G1 is oriented )
assume A1:
G1 c= G
; G1 is oriented
A2:
G1 is Subgraph of G
by A1, Def24;
A3:
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 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 implies x = y )
assume that A4:
x in the
carrier' of
G1
and A5:
y in the
carrier' of
G1
and A6:
the
Source of
G1 . x = the
Source of
G1 . y
and A7:
the
Target of
G1 . x = the
Target of
G1 . y
;
x = y
A8:
the
carrier' of
G1 c= the
carrier' of
G
by A2, Def18;
A9: the
Source of
G . x =
the
Source of
G1 . y
by A2, A4, A6, Def18
.=
the
Source of
G . y
by A2, A5, Def18
;
A10: the
Target of
G . x =
the
Target of
G1 . y
by A2, A4, A7, Def18
.=
the
Target of
G . y
by A2, A5, Def18
;
thus
x = y
by A4, A5, A8, A9, A10, Def5;
verum
end;
thus
G1 is oriented
by A3, Def5; verum