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 Th35;
S is AntiChain_of_Prefixes of T
proof
let x be object ; :: according to TARSKI:def 3,TREES_1:def 11 :: thesis: ( not x in S or x in T )
assume x in S ; :: thesis: x in T
then x = t by TARSKI:def 1;
hence x in T ; :: thesis: verum
end;
hence {t} is AntiChain_of_Prefixes of T ; :: thesis: verum