let x be set ; :: according to RELAT_1:def 1 :: thesis: ( not x in graph f or ex b₁, b₂ being set st x = [b₁,b₂] )
assume x in graph f ; :: thesis: ex b₁, b₂ being set st x = [b₁,b₂]
then ex y being finite set ex z being set st
( x = [y,z] & y in dom f & z in f . y ) by Def17;
hence ex b₁, b₂ being set st x = [b₁,b₂] ; :: thesis: verum