let X be set ; :: thesis: for V being Subset of X
for E being Subset of (TWOELEMENTSETS V)
for v1, v2 being set st v1 in V & v2 in V & v1 <> v2 & SimpleGraphStruct(# V,E #) in SIMPLEGRAPHS X holds
ex v1v2 being finite Subset of (TWOELEMENTSETS V) st
( v1v2 = E \/ {{v1,v2}} & SimpleGraphStruct(# V,v1v2 #) in SIMPLEGRAPHS X )
let V be Subset of X; :: thesis: for E being Subset of (TWOELEMENTSETS V)
for v1, v2 being set st v1 in V & v2 in V & v1 <> v2 & SimpleGraphStruct(# V,E #) in SIMPLEGRAPHS X holds
ex v1v2 being finite Subset of (TWOELEMENTSETS V) st
( v1v2 = E \/ {{v1,v2}} & SimpleGraphStruct(# V,v1v2 #) in SIMPLEGRAPHS X )
let E be Subset of (TWOELEMENTSETS V); :: thesis: for v1, v2 being set st v1 in V & v2 in V & v1 <> v2 & SimpleGraphStruct(# V,E #) in SIMPLEGRAPHS X holds
ex v1v2 being finite Subset of (TWOELEMENTSETS V) st
( v1v2 = E \/ {{v1,v2}} & SimpleGraphStruct(# V,v1v2 #) in SIMPLEGRAPHS X )
let v1, v2 be set ; :: thesis: ( v1 in V & v2 in V & v1 <> v2 & SimpleGraphStruct(# V,E #) in SIMPLEGRAPHS X implies ex v1v2 being finite Subset of (TWOELEMENTSETS V) st
( v1v2 = E \/ {{v1,v2}} & SimpleGraphStruct(# V,v1v2 #) in SIMPLEGRAPHS X ) )
set g = SimpleGraphStruct(# V,E #);
assume A1: ( v1 in V & v2 in V & not v1 = v2 & SimpleGraphStruct(# V,E #) in SIMPLEGRAPHS X ) ; :: thesis: ex v1v2 being finite Subset of (TWOELEMENTSETS V) st
( v1v2 = E \/ {{v1,v2}} & SimpleGraphStruct(# V,v1v2 #) in SIMPLEGRAPHS X )
then reconsider g = SimpleGraphStruct(# V,E #) as SimpleGraph of X by Def7;
A2: ( the carrier of g is finite Subset of X & the SEdges of g is finite Subset of (TWOELEMENTSETS V) ) by Th27;
then reconsider V = V as finite Subset of X ;
( E \/ {{v1,v2}} c= TWOELEMENTSETS V & E \/ {{v1,v2}} is finite )

proof

hereby :: according to TARSKI:def 3 :: thesis: E \/ {{v1,v2}} is finite

let e be set ; :: thesis: ( e in E \/ {{v1,v2}} implies b₁ in TWOELEMENTSETS V )
assume A3: e in E \/ {{v1,v2}} ; :: thesis: b₁ in TWOELEMENTSETS V

per cases ( e in E or e in {{v1,v2}} ) by A3, XBOOLE_0:def 3;

suppose e in E ; :: thesis: b₁ in TWOELEMENTSETS V

hence e in TWOELEMENTSETS V ; :: thesis: verum

end;

suppose e in {{v1,v2}} ; :: thesis: b₁ in TWOELEMENTSETS V

then A4: ( v1 in V & v2 in V & v1 <> v2 & e = {v1,v2} ) by A1, TARSKI:def 1;
then e is Subset of V by ZFMISC_1:38;
hence e in TWOELEMENTSETS V by A4, Th10; :: thesis: verum

end;

end;

end;

thus E \/ {{v1,v2}} is finite by A2; :: thesis: verum

end;

then reconsider E' = E \/ {{v1,v2}} as finite Subset of (TWOELEMENTSETS V) ;
SimpleGraphStruct(# V,E' #) in SIMPLEGRAPHS X ;
hence ex v1v2 being finite Subset of (TWOELEMENTSETS V) st
( v1v2 = E \/ {{v1,v2}} & SimpleGraphStruct(# V,v1v2 #) in SIMPLEGRAPHS X ) ; :: thesis: verum