let G1 be Graph; :: thesis: for G being oriented Graph st G1 c= G holds
G1 is oriented
let G be oriented Graph; :: thesis: ( G1 c= G implies G1 is oriented )
assume
G1 c= G
; :: thesis: G1 is oriented
then A1:
G1 is Subgraph of G
by Def23;
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 ;
:: thesis: ( 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 A2:
(
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 )
;
:: thesis: x = y
A3:
the
carrier' of
G1 c= the
carrier' of
G
by A1, Def17;
A4: the
Source of
G . x =
the
Source of
G1 . y
by A1, A2, Def17
.=
the
Source of
G . y
by A1, A2, Def17
;
the
Target of
G . x =
the
Target of
G1 . y
by A1, A2, Def17
.=
the
Target of
G . y
by A1, A2, Def17
;
hence
x = y
by A2, A3, A4, Def4;
:: thesis: verum
end;
hence
G1 is oriented
by Def4; :: thesis: verum