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

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

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

end;

given H0 being DLGraphComplement of G such that A2: H0 is G -Disomorphic ; :: thesis: G is self-DLcomplementary
let H be DLGraphComplement of G; :: according to GLIB_012:def 10 :: thesis: H is G -Disomorphic
H is H0 -Disomorphic by Th50;
hence H is G -Disomorphic by A2; :: thesis: verum