thus ( canCompleteGraph c is plain & canCompleteGraph c is c -vertex ) ; :: thesis: ( canCompleteGraph c is simple & canCompleteGraph c is complete )
(RelIncl c) \ (id c) misses id c by XBOOLE_1:79;
then (RelIncl c) \ (id c) is irreflexive by GLIBPRE0:11;
then canCompleteGraph c is loopless ;
hence canCompleteGraph c is simple ; :: thesis: canCompleteGraph c is complete

now :: thesis: for v, w being Vertex of (canCompleteGraph c) st v <> w holds
v,w are_adjacent

let v, w be Vertex of (canCompleteGraph c); :: thesis: ( v <> w implies b₁,b₂ are_adjacent )
assume v <> w ; :: thesis: b₁,b₂ are_adjacent
then A1: ( not [v,w] in id c & not [w,v] in id c ) by RELAT_1:def 10;

per cases ( v c= w or w in v ) by ORDINAL1:16;

suppose v c= w ; :: thesis: b₁,b₂ are_adjacent

then [v,w] in RelIncl c by WELLORD2:def 1;
then [v,w] in (RelIncl c) \ (id c) by A1, XBOOLE_0:def 5;
then [v,w] DJoins v,w, canCompleteGraph c by GLUNIR00:63;
then [v,w] Joins v,w, canCompleteGraph c by GLIB_000:16;
hence v,w are_adjacent by CHORD:def 3; :: thesis: verum

end;

suppose w in v ; :: thesis: b₁,b₂ are_adjacent

then w c= v by ORDINAL1:def 2;
then [w,v] in RelIncl c by WELLORD2:def 1;
then [w,v] in (RelIncl c) \ (id c) by A1, XBOOLE_0:def 5;
then [w,v] DJoins w,v, canCompleteGraph c by GLUNIR00:63;
then [w,v] Joins v,w, canCompleteGraph c by GLIB_000:16;
hence v,w are_adjacent by CHORD:def 3; :: thesis: verum

end;

end;

end;

hence canCompleteGraph c is complete by CHORD:def 6; :: thesis: verum