let X be set ; :: thesis:
let V be Subset of X; :: thesis:
let E be Subset of (TWOELEMENTSETS V); :: thesis:
let v1, v2 be set ; :: thesis:
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:
reconsider g = SimpleGraphStruct(# V,E #) as SimpleGraph of X by A3, Def4;
A4: the SEdges of g is finite Subset of (TWOELEMENTSETS V) by Th21;
the carrier of g is finite Subset of X by Th21;
then reconsider V = V as finite Subset of X ;
( E \/ {{v1,v2}} c= TWOELEMENTSETS V & E \/ {{v1,v2}} is finite )

hereby :: according to TARSKI:def 3 :: thesis:

end;

end;

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

end;