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