let G be SimpleGraph; :: thesis: for L, x, y being set st x in L & y in L & {x,y} in G holds
{x,y} in G SubgraphInducedBy L
let L, x, y be set ; :: thesis: ( x in L & y in L & {x,y} in G implies {x,y} in G SubgraphInducedBy L )
assume that
A: x in L and
B: y in L and
C: {x,y} in G ; :: thesis: {x,y} in G SubgraphInducedBy L
{x,y} c= L by A, B, ZFMISC_1:32;
hence {x,y} in G SubgraphInducedBy L by C, XBOOLE_0:def 4; :: thesis: verum