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
A1: x in G and
A2: 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 A1, Th27;
then ( x in {{}} \/ (singletons (Vertices G)) or x in Edges G ) by XBOOLE_0:def 3;
then A3: ( 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 A3, A2, 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
A4: x = f and
A5: f is 1 -element ;
consider v being set such that
A6: v in Vertices G and
A7: f = {v} by A5, Th9;
thus ( ex y being set st
( x = {y} & y in Vertices G ) or x in Edges G ) by A7, A6, A4; :: 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;