let G1 be _Graph; :: thesis:
let G2 be Subgraph of G1; :: thesis:
let v1 be Vertex of G1; :: thesis:
let v2 be Vertex of G2; :: thesis:
assume A1: v1 = v2 ; :: thesis:

let v be object ; :: thesis:
assume v in v2 .inNeighbors() ; :: thesis:
then consider e being object such that
A2: e DJoins v,v2,G2 by Th69;
e DJoins v,v1,G1 by A1, A2, Th72;
hence v in v1 .inNeighbors() by Th69; :: thesis:

end;

hence v2 .inNeighbors() c= v1 .inNeighbors() ; :: thesis:

let v be object ; :: thesis:
assume v in v2 .outNeighbors() ; :: thesis:
then consider e being object such that
A3: e DJoins v2,v,G2 by Th70;
e DJoins v1,v,G1 by A1, A3, Th72;
hence v in v1 .outNeighbors() by Th70; :: thesis:

end;

hence v2 .outNeighbors() c= v1 .outNeighbors() ; :: thesis:
let v be object ; :: according to TARSKI:def 3 :: thesis:
assume v in v2 .allNeighbors() ; :: thesis:
then consider e being object such that
A4: e Joins v2,v,G2 by Th71;
e Joins v1,v,G1 by A1, A4, Lm4;
hence v in v1 .allNeighbors() by Th71; :: thesis: