let T be Tree; :: thesis: ( {} is AntiChain_of_Prefixes of T & {{}} is AntiChain_of_Prefixes of T )
{} is AntiChain_of_Prefixes-like ;
then reconsider S = {} as AntiChain_of_Prefixes ;
S c= T ;
hence {} is AntiChain_of_Prefixes of T by Def11; :: thesis: {{}} is AntiChain_of_Prefixes of T
reconsider S = {{}} 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 = {} by TARSKI:def 1;
hence x in T by Th21; :: thesis: verum
end;
hence {{}} is AntiChain_of_Prefixes of T ; :: thesis: verum