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

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in X or x in T )
assume x in X ; :: thesis: x in T
then x = the Element of T by A1, TARSKI:def 1;
hence x in T ; :: thesis: verum

end;

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