let w be FinSequence; :: thesis: {w} is AntiChain_of_Prefixes-like
thus for x being set st x in {w} holds
x is FinSequence by TARSKI:def 1; :: according to TREES_1:def 10 :: thesis: for p1, p2 being FinSequence st p1 in {w} & p2 in {w} & p1 <> p2 holds
not p1,p2 are_c=-comparable
let p1, p2 be FinSequence; :: thesis: ( p1 in {w} & p2 in {w} & p1 <> p2 implies not p1,p2 are_c=-comparable )
assume that
A1: p1 in {w} and
A2: p2 in {w} ; :: thesis: ( not p1 <> p2 or not p1,p2 are_c=-comparable )
p1 = w by A1, TARSKI:def 1;
hence ( not p1 <> p2 or not p1,p2 are_c=-comparable ) by A2, TARSKI:def 1; :: thesis: verum