let B, C be antichain; :: thesis: B ^ C is antichain-like
let p be FinSequence; :: according to POLNOT_1:def 16 :: thesis: for q being FinSequence st p in B ^ C & p ^ q in B ^ C holds
q = {}
let q be FinSequence; :: thesis: ( p in B ^ C & p ^ q in B ^ C implies q = {} )
assume that
A3: p in B ^ C and
A4: p ^ q in B ^ C ; :: thesis: q = {}
consider r, s being FinSequence such that
A7: p = r ^ s and
A8: r in B and
A9: s in C by A3, Def2;
consider t, u being FinSequence such that
A10: p ^ q = t ^ u and
A11: t in B and
A12: u in C by A4, Def2;
t ^ u = r ^ (s ^ q) by A7, A10, FINSEQ_1:32;
then u = s ^ q by A8, A11, Th43;
hence q = {} by A9, A12, Def16; :: thesis: verum