let T be Tree; :: thesis: ( {} is AntiChain_of_Prefixes of T & {{} } is AntiChain_of_Prefixes of T )
{} is AntiChain_of_Prefixes-like

proof

thus for x being set st x in {} holds
x is FinSequence ; :: according to TREES_1:def 13 :: thesis: for p1, p2 being FinSequence st p1 in {} & p2 in {} & p1 <> p2 holds
not p1,p2 are_c=-comparable
let p1, p2 be FinSequence; :: thesis: ( p1 in {} & p2 in {} & p1 <> p2 implies not p1,p2 are_c=-comparable )
thus ( p1 in {} & p2 in {} & p1 <> p2 implies not p1,p2 are_c=-comparable ) ; :: thesis: verum

end;

then reconsider S = {} as AntiChain_of_Prefixes ;
S c= T by XBOOLE_1:2;
hence {} is AntiChain_of_Prefixes of T by Def14; :: thesis: {{} } is AntiChain_of_Prefixes of T
reconsider S = {{} } as AntiChain_of_Prefixes by Th70;
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 x in S ; :: thesis: x in T
then x = {} by TARSKI:def 1;
hence x in T by Th47; :: thesis: verum

end;

hence {{} } is AntiChain_of_Prefixes of T ; :: thesis: verum