let T be Tree; :: thesis: for t1, t2 being Element of T st not t1,t2 are_c=-comparable holds
{t1,t2} is AntiChain_of_Prefixes of T
let t1, t2 be Element of T; :: thesis: ( not t1,t2 are_c=-comparable implies {t1,t2} is AntiChain_of_Prefixes of T )
assume not t1,t2 are_c=-comparable ; :: thesis: {t1,t2} is AntiChain_of_Prefixes of T
then reconsider A = {t1,t2} as AntiChain_of_Prefixes by Th71;
A is AntiChain_of_Prefixes of T

proof

let x be set ; :: according to TARSKI:def 3,TREES_1:def 14 :: thesis: ( not x in A or x in T )
assume x in A ; :: thesis: x in T
then ( x = t1 or x = t2 ) by TARSKI:def 2;
hence x in T ; :: thesis: verum

end;

hence {t1,t2} is AntiChain_of_Prefixes of T ; :: thesis: verum