let W be Tree; :: thesis: {{} } is Chain of W
A1: {} in W by TREES_1:47;
reconsider S = {{} } as Subset of W by A1, ZFMISC_1:37;
A2: S is Chain of W

proof

let p be FinSequence of NAT ; :: according to TREES_2:def 3 :: thesis: for q being FinSequence of NAT st p in S & q in S holds
p,q are_c=-comparable
let q be FinSequence of NAT ; :: thesis: ( p in S & q in S implies p,q are_c=-comparable )
assume that
A3: p in S and
A4: q in S ; :: thesis: p,q are_c=-comparable
A5: p = {} by A3, TARSKI:def 1;
thus p,q are_c=-comparable by A4, A5, TARSKI:def 1; :: thesis: verum

end;

thus {{} } is Chain of W by A2; :: thesis: verum