let G be non empty RelStr ; :: thesis: for H being non empty full SubRelStr of G st G is N-free holds
H is N-free
let H be non empty full SubRelStr of G; :: thesis: ( G is N-free implies H is N-free )
assume A1: G is N-free ; :: thesis: H is N-free
A2: G embeds H by Th22;
assume not H is N-free ; :: thesis: contradiction
then H embeds Necklace 4 by NECKLA_2:def 1;
then G embeds Necklace 4 by A2, NECKLACE:12;
hence contradiction by A1, NECKLA_2:def 1; :: thesis: verum