let G be SimpleGraph; :: thesis: for x being set st x in G & x <> {} & ( for y being set holds
( not x = {y} or not y in Vertices G ) ) holds
x in Edges G
let x be set ; :: thesis: ( x in G & x <> {} & ( for y being set holds
( not x = {y} or not y in Vertices G ) ) implies x in Edges G )
assume that
A: x in G and
B: x <> {} ; :: thesis: ( ex y being set st
( x = {y} & y in Vertices G ) or x in Edges G )
x in ({{}} \/ (singletons (Vertices G))) \/ (Edges G) by A, SG0;
then ( x in {{}} \/ (singletons (Vertices G)) or x in Edges G ) by XBOOLE_0:def 3;
then C: ( x in {{}} or x in singletons (Vertices G) or x in Edges G ) by XBOOLE_0:def 3;

per cases ( x in singletons (Vertices G) or x in Edges G ) by C, B, TARSKI:def 1;

suppose x in singletons (Vertices G) ; :: thesis: ( ex y being set st
( x = {y} & y in Vertices G ) or x in Edges G )

then consider f being Subset of (Vertices G) such that
A2: x = f and
B2: f is 1 -element ;
consider v being set such that
C2: v in Vertices G and
D2: f = {v} by B2, BSPACEdef9;
thus ( ex y being set st
( x = {y} & y in Vertices G ) or x in Edges G ) by D2, C2, A2; :: thesis: verum

end;

suppose x in Edges G ; :: thesis: ( ex y being set st
( x = {y} & y in Vertices G ) or x in Edges G )

hence ( ex y being set st
( x = {y} & y in Vertices G ) or x in Edges G ) ; :: thesis: verum

end;

end;