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 A1: not t1,t2 are_c=-comparable ; :: thesis: {t1,t2} is AntiChain_of_Prefixes of T
reconsider A = {t1,t2} as AntiChain_of_Prefixes by A1, Th71;
A2: 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 A3: x in A ; :: thesis: x in T
A4: ( x = t1 or x = t2 ) by A3, TARSKI:def 2;
thus x in T by A4; :: thesis: verum

end;

thus {t1,t2} is AntiChain_of_Prefixes of T by A2; :: thesis: verum