let G be non empty irreflexive RelStr ; :: thesis: ( G is N-free iff ComplRelStr G is N-free )

thus ( G is N-free implies ComplRelStr G is N-free ) :: thesis: ( ComplRelStr G is N-free implies G is N-free )

assume not G is N-free ; :: thesis: contradiction

then G embeds Necklace 4 by NECKLA_2:def 1;

then ComplRelStr G embeds Necklace 4 by Th24;

hence contradiction by A2, NECKLA_2:def 1; :: thesis: verum

thus ( G is N-free implies ComplRelStr G is N-free ) :: thesis: ( ComplRelStr G is N-free implies G is N-free )

proof

assume A2:
ComplRelStr G is N-free
; :: thesis: G is N-free
assume A1:
G is N-free
; :: thesis: ComplRelStr G is N-free

assume not ComplRelStr G is N-free ; :: thesis: contradiction

then ComplRelStr G embeds Necklace 4 by NECKLA_2:def 1;

then G embeds Necklace 4 by Th24;

hence contradiction by A1, NECKLA_2:def 1; :: thesis: verum

end;assume not ComplRelStr G is N-free ; :: thesis: contradiction

then ComplRelStr G embeds Necklace 4 by NECKLA_2:def 1;

then G embeds Necklace 4 by Th24;

hence contradiction by A1, NECKLA_2:def 1; :: thesis: verum

assume not G is N-free ; :: thesis: contradiction

then G embeds Necklace 4 by NECKLA_2:def 1;

then ComplRelStr G embeds Necklace 4 by Th24;

hence contradiction by A2, NECKLA_2:def 1; :: thesis: verum