let P be FinSequence-membered set ; :: thesis: for a being object st ( for p being FinSequence st p in P holds
dom p = a ) holds
P is antichain-like
let a be object ; :: thesis: ( ( for p being FinSequence st p in P holds
dom p = a ) implies P is antichain-like )
assume A1: for p being FinSequence st p in P holds
dom p = a ; :: thesis: P is antichain-like
for p, q being FinSequence st p in P & q in P holds
dom p = dom q

proof

let p, q be FinSequence; :: thesis: ( p in P & q in P implies dom p = dom q )
assume that
A2: p in P and
A3: q in P ; :: thesis: dom p = dom q
dom p = a by A1, A2
.= dom q by A1, A3 ;
hence dom p = dom q ; :: thesis: verum

end;

hence P is antichain-like by Th44; :: thesis: verum