let P be FinSequence-membered set ; :: thesis: ( P is antichain-like iff for p, q being FinSequence st p in P & p ^ q in P holds
p = p ^ q )
thus ( P is antichain-like implies for p, q being FinSequence st p in P & p ^ q in P holds
p = p ^ q ) :: thesis: ( ( for p, q being FinSequence st p in P & p ^ q in P holds
p = p ^ q ) implies P is antichain-like )

proof

assume A1: P is antichain-like ; :: thesis: for p, q being FinSequence st p in P & p ^ q in P holds
p = p ^ q
let p, q be FinSequence; :: thesis: ( p in P & p ^ q in P implies p = p ^ q )
assume ( p in P & p ^ q in P ) ; :: thesis: p = p ^ q
then q = {} by A1;
hence p = p ^ q by FINSEQ_1:34; :: thesis: verum

end;

thus ( ( for p, q being FinSequence st p in P & p ^ q in P holds
p = p ^ q ) implies P is antichain-like ) by FINSEQ_1:87; :: thesis: verum