let G2 be _Graph; for G1 being Supergraph of G2
for x, y being set
for e being object holds
( ( e Joins x,y,G2 implies e Joins x,y,G1 ) & ( e DJoins x,y,G2 implies e DJoins x,y,G1 ) & ( e SJoins x,y,G2 implies e SJoins x,y,G1 ) & ( e DSJoins x,y,G2 implies e DSJoins x,y,G1 ) )
let G1 be Supergraph of G2; for x, y being set
for e being object holds
( ( e Joins x,y,G2 implies e Joins x,y,G1 ) & ( e DJoins x,y,G2 implies e DJoins x,y,G1 ) & ( e SJoins x,y,G2 implies e SJoins x,y,G1 ) & ( e DSJoins x,y,G2 implies e DSJoins x,y,G1 ) )
let x, y be set ; for e being object holds
( ( e Joins x,y,G2 implies e Joins x,y,G1 ) & ( e DJoins x,y,G2 implies e DJoins x,y,G1 ) & ( e SJoins x,y,G2 implies e SJoins x,y,G1 ) & ( e DSJoins x,y,G2 implies e DSJoins x,y,G1 ) )
let e be object ; ( ( e Joins x,y,G2 implies e Joins x,y,G1 ) & ( e DJoins x,y,G2 implies e DJoins x,y,G1 ) & ( e SJoins x,y,G2 implies e SJoins x,y,G1 ) & ( e DSJoins x,y,G2 implies e DSJoins x,y,G1 ) )
G2 is Subgraph of G1
by Th61;
hence
( ( e Joins x,y,G2 implies e Joins x,y,G1 ) & ( e DJoins x,y,G2 implies e DJoins x,y,G1 ) & ( e SJoins x,y,G2 implies e SJoins x,y,G1 ) & ( e DSJoins x,y,G2 implies e DSJoins x,y,G1 ) )
by GLIB_000:72; verum