thus ( G is antichain-like implies for g, h being FinSequence of D st g in G & g ^ h in G holds
h = <*> D ) ; :: thesis: ( ( for g, h being FinSequence of D st g in G & g ^ h in G holds
h = <*> D ) implies G is antichain-like )
assume A1: for g, h being FinSequence of D st g in G & g ^ h in G holds
h = <*> D ; :: thesis: G is antichain-like
for p, q being FinSequence st p in G & p ^ q in G holds
q = {}

proof

let p, q be FinSequence; :: thesis: ( p in G & p ^ q in G implies q = {} )
assume that
A3: p in G and
A4: p ^ q in G ; :: thesis: q = {}
p ^ q is FinSequence of D by A4, FINSEQ_1:def 11;
then reconsider p = p, q = q as FinSequence of D by FINSEQ_1:36;
p ^ q in G by A4;
hence q = {} by A1, A3; :: thesis: verum

end;

hence G is antichain-like ; :: thesis: verum