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

take X ; :: thesis: not X is empty

thus not X is empty by A1; :: thesis: verum

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

then reconsider X = X as AntiChain_of_Prefixes of T by A2, TREES_1:def 11;
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;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

take X ; :: thesis: not X is empty

thus not X is empty by A1; :: thesis: verum