let c be non empty Cardinal; :: thesis: for v being Vertex of (canCompleteGraph c) holds
( v .inNeighbors() = v & v .outNeighbors() = c \ (succ v) )
let v be Vertex of (canCompleteGraph c); :: thesis: ( v .inNeighbors() = v & v .outNeighbors() = c \ (succ v) )

now :: thesis: for x being object holds
( ( x in v .inNeighbors() implies x in v ) & ( x in v implies x in v .inNeighbors() ) )

let x be object ; :: thesis: ( ( x in v .inNeighbors() implies x in v ) & ( x in v implies x in v .inNeighbors() ) )

hereby :: thesis: ( x in v implies x in v .inNeighbors() )

assume A1: x in v .inNeighbors() ; :: thesis: x in v
then reconsider a = x as Ordinal ;
consider e being object such that
A2: e DJoins x,v, canCompleteGraph c by A1, GLIB_000:69;
e = [x,v] by A2, GLUNIR00:64;
then [x,v] in (RelIncl c) \ (id c) by A2, GLUNIR00:63;
then [x,v] in RelIncl c by XBOOLE_0:def 5;
then A3: a c= v by ORDINAL6:8;
x <> v by A2, GLIB_000:136;
then not v c= a by A3, XBOOLE_0:def 10;
then a in v by ORDINAL1:16;
hence x in v ; :: thesis: verum

end;

assume A4: x in v ; :: thesis: x in v .inNeighbors()
then reconsider a = x as Vertex of (canCompleteGraph c) by ORDINAL1:10;
a <> v

proof

assume a = v ; :: thesis: contradiction
then v in v by A4;
hence contradiction ; :: thesis: verum

end;

then ( a c= v & a <> v ) by A4, ORDINAL1:def 2;
then ( [a,v] in RelIncl c & not [a,v] in id c ) by WELLORD2:def 1, RELAT_1:def 10;
then [a,v] in (RelIncl c) \ (id c) by XBOOLE_0:def 5;
hence x in v .inNeighbors() by GLIB_000:69, GLUNIR00:63; :: thesis: verum

end;

hence v .inNeighbors() = v by TARSKI:2; :: thesis: v .outNeighbors() = c \ (succ v)

now :: thesis: for x being object holds
( ( x in v .outNeighbors() implies x in c \ (succ v) ) & ( x in c \ (succ v) implies x in v .outNeighbors() ) )

let x be object ; :: thesis: ( ( x in v .outNeighbors() implies x in c \ (succ v) ) & ( x in c \ (succ v) implies x in v .outNeighbors() ) )

hereby :: thesis: ( x in c \ (succ v) implies x in v .outNeighbors() )

assume A5: x in v .outNeighbors() ; :: thesis: x in c \ (succ v)
then reconsider a = x as Vertex of (canCompleteGraph c) ;
consider e being object such that
A6: e DJoins v,x, canCompleteGraph c by A5, GLIB_000:70;
e = [v,x] by A6, GLUNIR00:64;
then [v,x] in (RelIncl c) \ (id c) by A6, GLUNIR00:63;
then [v,x] in RelIncl c by XBOOLE_0:def 5;
then A7: v c= a by ORDINAL6:8;
x <> v by A6, GLIB_000:136;
then not a c= v by A7, XBOOLE_0:def 10;
then not succ a c= succ v by ORDINAL2:1;
then not a in succ v by ORDINAL1:21;
hence x in c \ (succ v) by XBOOLE_0:def 5; :: thesis: verum

end;

assume x in c \ (succ v) ; :: thesis: x in v .outNeighbors()
then A8: ( x in c & not x in succ v ) by XBOOLE_0:def 5;
then reconsider a = x as Vertex of (canCompleteGraph c) ;
not succ a c= succ v by A8, ORDINAL1:21;
then A9: ( v in a & v <> a ) by ORDINAL1:16, ORDINAL2:1;
then v c= a by ORDINAL1:def 2;
then ( [v,a] in RelIncl c & not [v,a] in id c ) by A9, WELLORD2:def 1, RELAT_1:def 10;
then [v,a] in (RelIncl c) \ (id c) by XBOOLE_0:def 5;
hence x in v .outNeighbors() by GLIB_000:70, GLUNIR00:63; :: thesis: verum

end;

hence v .outNeighbors() = c \ (succ v) by TARSKI:2; :: thesis: verum