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