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 10 :: 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 that
A2: q1 in {p1,p2} and
A3: q2 in {p1,p2} ; :: thesis: ( not q1 <> q2 or not q1,q2 are_c=-comparable )
A4: ( q1 = p1 or q1 = p2 ) by A2, TARSKI:def 2;
( q2 = p1 or q2 = p2 ) by A3, TARSKI:def 2;
hence ( not q1 <> q2 or not q1,q2 are_c=-comparable ) by A1, A4; :: thesis: verum