let G be _Graph; :: thesis: ( G is self-Dcomplementary iff ex H being DGraphComplement of G st H is G -Disomorphic )

hereby :: thesis: ( ex H being DGraphComplement of G st H is G -Disomorphic implies G is self-Dcomplementary )

assume A1: G is self-Dcomplementary ; :: thesis: ex H being DGraphComplement of G st H is G -Disomorphic
reconsider H = the DGraphComplement of G as DGraphComplement of G ;
take H = H; :: thesis: H is G -Disomorphic
thus H is G -Disomorphic by A1; :: thesis: verum

end;

given H0 being DGraphComplement of G such that A2: H0 is G -Disomorphic ; :: thesis: G is self-Dcomplementary
let H be DGraphComplement of G; :: according to GLIB_012:def 12 :: thesis: H is G -Disomorphic
H is H0 -Disomorphic by Th85;
hence H is G -Disomorphic by A2; :: thesis: verum