consider w being Element of T;
consider X being set such that
A1: X = {w} ;
A2: X is AntiChain_of_Prefixes-like by A1, TREES_1:70;
A3: X c= T

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in X or x in T )
assume A4: x in X ; :: thesis: x in T
A5: x = w by A1, A4, TARSKI:def 1;
thus x in T by A5; :: thesis: verum

end;

reconsider X = X as AntiChain_of_Prefixes of T by A2, A3, TREES_1:def 14;
take X ; :: thesis: not X is empty
thus not X is empty by A1; :: thesis: verum