let T be Tree; :: thesis: for t being Element of T holds {t} is AntiChain_of_Prefixes of T
let t be Element of T; :: thesis: {t} is AntiChain_of_Prefixes of T
reconsider S = {t} as AntiChain_of_Prefixes by Th70;
A1: S is AntiChain_of_Prefixes of T

proof

let x be set ; :: according to TARSKI:def 3,TREES_1:def 14 :: thesis: ( not x in S or x in T )
assume A2: x in S ; :: thesis: x in T
A3: x = t by A2, TARSKI:def 1;
thus x in T by A3; :: thesis: verum

end;

thus {t} is AntiChain_of_Prefixes of T by A1; :: thesis: verum