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 Th36;
A is AntiChain_of_Prefixes of T
proof
let x be object ; :: according to TARSKI:def 3,TREES_1:def 11 :: 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