take {} ; :: thesis: {} is AntiChain_of_Prefixes-like
thus for x being set st x in {} holds
x is FinSequence ; :: according to TREES_1:def 10 :: thesis: for p1, p2 being FinSequence st p1 in {} & p2 in {} & p1 <> p2 holds
not p1,p2 are_c=-comparable
let p1, p2 be FinSequence; :: thesis: ( p1 in {} & p2 in {} & p1 <> p2 implies not p1,p2 are_c=-comparable )
thus ( p1 in {} & p2 in {} & p1 <> p2 implies not p1,p2 are_c=-comparable ) ; :: thesis: verum