let W be Tree; :: thesis: {} is Chain of W
reconsider S = {} as Subset of W by XBOOLE_1:2;
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 )
thus ( p in S & q in S implies p,q are_c=-comparable ) ; :: thesis: verum
end;
hence {} is Chain of W ; :: thesis: verum