let G be _Graph; :: thesis: ( G is self-Lcomplementary iff ex H being LGraphComplement of G st H is G -isomorphic )

hereby :: thesis: ( ex H being LGraphComplement of G st H is G -isomorphic implies G is self-Lcomplementary )

assume A1: G is self-Lcomplementary ; :: thesis: ex H being LGraphComplement of G st H is G -isomorphic
reconsider H = the LGraphComplement of G as LGraphComplement of G ;
take H = H; :: thesis: H is G -isomorphic
thus H is G -isomorphic by A1; :: thesis: verum

end;

given H0 being LGraphComplement of G such that A2: H0 is G -isomorphic ; :: thesis: G is self-Lcomplementary
let H be LGraphComplement of G; :: according to GLIB_012:def 11 :: thesis: H is G -isomorphic
H is H0 -isomorphic by Th68;
hence H is G -isomorphic by A2; :: thesis: verum