let X be set ; :: thesis: for V being Subset of
for E being Subset of
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 st
( v1v2 = E \/ {{v1,v2}} & SimpleGraphStruct(# V,v1v2 #) in SIMPLEGRAPHS X )
let V be Subset of ; :: thesis: for E being Subset of
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 st
( v1v2 = E \/ {{v1,v2}} & SimpleGraphStruct(# V,v1v2 #) in SIMPLEGRAPHS X )
let E be Subset of ; :: 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 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 st
( v1v2 = E \/ {{v1,v2}} & SimpleGraphStruct(# V,v1v2 #) in SIMPLEGRAPHS X ) )
set g = SimpleGraphStruct(# V,E #);
assume that
A1: ( v1 in V & v2 in V ) and
A2: not v1 = v2 and
A3: SimpleGraphStruct(# V,E #) in SIMPLEGRAPHS X ; :: thesis: ex v1v2 being finite Subset of st
( v1v2 = E \/ {{v1,v2}} & SimpleGraphStruct(# V,v1v2 #) in SIMPLEGRAPHS X )
reconsider g = SimpleGraphStruct(# V,E #) as SimpleGraph of X by A3, Def7;
A4: the SEdges of g is finite Subset of by Th27;
the carrier of g is finite Subset of by Th27;
then reconsider V = V as finite Subset of ;
( 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 A5: e in E \/ {{v1,v2}} ; :: thesis: b₁ in TWOELEMENTSETS V

per cases ( e in E or e in {{v1,v2}} ) by A5, 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 A6: e = {v1,v2} by TARSKI:def 1;
then e is Subset of by A1, ZFMISC_1:38;
hence e in TWOELEMENTSETS V by A1, A2, A6, Th10; :: thesis: verum

end;

end;

end;

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

end;

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