let T be Tree; :: thesis: ( {} is AntiChain_of_Prefixes of T & {{} } is AntiChain_of_Prefixes of T )
A1: {} 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;

reconsider S = {} as AntiChain_of_Prefixes by A1;
A2: S c= T by XBOOLE_1:2;
thus {} is AntiChain_of_Prefixes of T by A2, Def14; :: thesis: {{} } is AntiChain_of_Prefixes of T
reconsider S = {{} } as AntiChain_of_Prefixes by Th70;
A3: 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 A4: x in S ; :: thesis: x in T
A5: x = {} by A4, TARSKI:def 1;
thus x in T by A5, Th47; :: thesis: verum

end;

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