let G1 be simple _Graph; :: thesis: for G2 being GraphComplement of G1
for v1 being Vertex of G1
for v2 being Vertex of G2 st v1 = v2 & G1 .order() = 2 holds
( ( v1 is endvertex implies v2 is isolated ) & ( v2 is isolated implies v1 is endvertex ) & ( v1 is isolated implies v2 is endvertex ) & ( v2 is endvertex implies v1 is isolated ) )
let G2 be GraphComplement of G1; :: thesis: for v1 being Vertex of G1
for v2 being Vertex of G2 st v1 = v2 & G1 .order() = 2 holds
( ( v1 is endvertex implies v2 is isolated ) & ( v2 is isolated implies v1 is endvertex ) & ( v1 is isolated implies v2 is endvertex ) & ( v2 is endvertex implies v1 is isolated ) )
let v1 be Vertex of G1; :: thesis: for v2 being Vertex of G2 st v1 = v2 & G1 .order() = 2 holds
( ( v1 is endvertex implies v2 is isolated ) & ( v2 is isolated implies v1 is endvertex ) & ( v1 is isolated implies v2 is endvertex ) & ( v2 is endvertex implies v1 is isolated ) )
let v2 be Vertex of G2; :: thesis: ( v1 = v2 & G1 .order() = 2 implies ( ( v1 is endvertex implies v2 is isolated ) & ( v2 is isolated implies v1 is endvertex ) & ( v1 is isolated implies v2 is endvertex ) & ( v2 is endvertex implies v1 is isolated ) ) )
assume A1: ( v1 = v2 & G1 .order() = 2 ) ; :: thesis: ( ( v1 is endvertex implies v2 is isolated ) & ( v2 is isolated implies v1 is endvertex ) & ( v1 is isolated implies v2 is endvertex ) & ( v2 is endvertex implies v1 is isolated ) )
then ( G1 is GraphComplement of G2 & G2 .order() = 2 ) by Th110, Th111;
hence ( ( v1 is endvertex implies v2 is isolated ) & ( v2 is isolated implies v1 is endvertex ) & ( v1 is isolated implies v2 is endvertex ) & ( v2 is endvertex implies v1 is isolated ) ) by A1, Th115; :: thesis: verum