let G be SimpleGraph; 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 ; ( 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
; {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; verum