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 set ; :: thesis:
assume v in v2 .inNeighbors() ; :: thesis:
then consider e being set such that
A2: e DJoins v,v2,G2 by Th72;
e DJoins v,v1,G1 by A1, A2, Th75;
hence v in v1 .inNeighbors() by Th72; :: thesis:

end;

hence v2 .inNeighbors() c= v1 .inNeighbors() by TARSKI:def 3; :: thesis:

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

end;

hence v2 .outNeighbors() c= v1 .outNeighbors() by TARSKI:def 3; :: thesis:

let v be set ; :: thesis:
assume v in v2 .allNeighbors() ; :: thesis:
then consider e being set such that
A4: e Joins v2,v,G2 by Th74;
e Joins v1,v,G1 by A1, A4, Lm5;
hence v in v1 .allNeighbors() by Th74; :: thesis:

end;

hence v2 .allNeighbors() c= v1 .allNeighbors() by TARSKI:def 3; :: thesis: