let F be non empty Graph-yielding Function; for x, y being Element of dom F holds [:{[(the_Vertices_of F),x]},((the_Vertices_of F) . x):] misses the_Vertices_of (F . y)
let x, y be Element of dom F; [:{[(the_Vertices_of F),x]},((the_Vertices_of F) . x):] misses the_Vertices_of (F . y)
[:{[(the_Vertices_of F),x]},((the_Vertices_of F) . x):] /\ (the_Vertices_of (F . y)) = {}
proof
assume A1:
[:{[(the_Vertices_of F),x]},((the_Vertices_of F) . x):] /\ (the_Vertices_of (F . y)) <> {}
;
contradiction
set z = the
Element of
[:{[(the_Vertices_of F),x]},((the_Vertices_of F) . x):] /\ (the_Vertices_of (F . y));
A2:
( the
Element of
[:{[(the_Vertices_of F),x]},((the_Vertices_of F) . x):] /\ (the_Vertices_of (F . y)) in [:{[(the_Vertices_of F),x]},((the_Vertices_of F) . x):] & the
Element of
[:{[(the_Vertices_of F),x]},((the_Vertices_of F) . x):] /\ (the_Vertices_of (F . y)) in the_Vertices_of (F . y) )
by A1, XBOOLE_0:def 4;
then consider a,
b being
object such that A3:
(
a in {[(the_Vertices_of F),x]} &
b in (the_Vertices_of F) . x & the
Element of
[:{[(the_Vertices_of F),x]},((the_Vertices_of F) . x):] /\ (the_Vertices_of (F . y)) = [a,b] )
by ZFMISC_1:def 2;
A4:
a = [(the_Vertices_of F),x]
by A3, TARSKI:def 1;
reconsider Z = the
Element of
[:{[(the_Vertices_of F),x]},((the_Vertices_of F) . x):] /\ (the_Vertices_of (F . y)),
A =
a,
M =
[y,(the_Vertices_of (F . y))] as
set by TARSKI:1;
A5:
the_Vertices_of (F . y) in {y,(the_Vertices_of (F . y))}
by TARSKI:def 2;
{y,(the_Vertices_of (F . y))} in {{y,(the_Vertices_of (F . y))},{y}}
by TARSKI:def 2;
then A6:
{y,(the_Vertices_of (F . y))} in M
by TARSKI:def 5;
A7:
the_Vertices_of (F . y) = (the_Vertices_of F) . y
by Def8;
dom F = dom (the_Vertices_of F)
by Def4;
then A8:
[y,(the_Vertices_of (F . y))] in the_Vertices_of F
by A7, FUNCT_1:1;
A9:
the_Vertices_of F in {(the_Vertices_of F)}
by TARSKI:def 1;
{(the_Vertices_of F)} in {{(the_Vertices_of F),x},{(the_Vertices_of F)}}
by TARSKI:def 2;
then A10:
{(the_Vertices_of F)} in A
by A4, TARSKI:def 5;
A11:
a in {a}
by A3, A4;
{a} in {{a,b},{a}}
by TARSKI:def 2;
then A12:
{a} in Z
by A3, TARSKI:def 5;
thus
contradiction
by A2, A5, A6, A8, A9, A10, A11, A12, GLIBPRE1:2;
verum
end;
hence
[:{[(the_Vertices_of F),x]},((the_Vertices_of F) . x):] misses the_Vertices_of (F . y)
by XBOOLE_0:def 7; verum