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 )
proof
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 A2: ComplRelStr G is N-free ; :: thesis: 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