let P be FinSequence-membered set ; :: thesis: ( P is trivial implies P is antichain-like )
assume A1: P is trivial ; :: thesis: P is antichain-like
let p be FinSequence; :: according to POLNOT_1:def 16 :: thesis: for q being FinSequence st p in P & p ^ q in P holds
q = {}
let q be FinSequence; :: thesis: ( p in P & p ^ q in P implies q = {} )
assume ( p in P & p ^ q in P ) ; :: thesis: q = {}
then p = p ^ q by A1, ZFMISC_1:def 10;
hence q = {} by FINSEQ_1:87; :: thesis: verum