let X be set ; :: thesis: ( X = F _E implies X is empty )
assume A2: X = F _E ; :: thesis: X is empty
F _E is empty

proof

assume A3: not F _E is empty ; :: thesis: contradiction
set e = the Element of dom (F _E);
(the_Source_of G1) . the Element of dom (F _E) in dom (F _V) by A3, Th5;
hence contradiction ; :: thesis: verum

end;

hence X is empty by A2; :: thesis: verum