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

assume A2: X = F _E ; :: thesis: X is empty

F _E is empty

proof

hence
X is empty
by A2; :: thesis: verum
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;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