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

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