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
A1: x in L and
A2: y in L and
A3: {x,y} in G ; :: thesis: {x,y} in G SubgraphInducedBy L
{x,y} c= L by A1, A2, ZFMISC_1:32;
hence {x,y} in G SubgraphInducedBy L by A3, XBOOLE_0:def 4; :: thesis: verum