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
G1 c= G
; G1 is oriented
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 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 A2:
x in the
carrier' of
G1
and A3:
y in the
carrier' of
G1
and A4:
the
Source of
G1 . x = the
Source of
G1 . y
and A5:
the
Target of
G1 . x = the
Target of
G1 . y
;
x = y
A6:
the
carrier' of
G1 c= the
carrier' of
G
by A1, Def18;
A7: the
Source of
G . x =
the
Source of
G1 . y
by A1, A2, A4, Def18
.=
the
Source of
G . y
by A1, A3, Def18
;
the
Target of
G . x =
the
Target of
G1 . y
by A1, A2, A5, Def18
.=
the
Target of
G . y
by A1, A3, Def18
;
hence
x = y
by A2, A3, A6, A7, Def7;
verum
end;
hence
G1 is oriented
; verum