let W be Tree; :: thesis: for L being Level of W holds L is AntiChain_of_Prefixes of W
let L be Level of W; :: thesis: L is AntiChain_of_Prefixes of W
consider n being Nat such that
A1: L = { w where w is Element of W : len w = n } by Def4;
L is AntiChain_of_Prefixes-like

proof

thus for x being set st x in L holds
x is FinSequence :: according to TREES_1:def 10 :: thesis: for b₁, b₂ being set holds
( not b₁ in L or not b₂ in L or b₁ = b₂ or not b₁,b₂ are_c=-comparable )

proof

let x be set ; :: thesis: ( x in L implies x is FinSequence )
assume x in L ; :: thesis: x is FinSequence
then x is Element of W ;
hence x is FinSequence ; :: thesis: verum

end;

let v1, v2 be FinSequence; :: thesis: ( not v1 in L or not v2 in L or v1 = v2 or not v1,v2 are_c=-comparable )
assume v1 in L ; :: thesis: ( not v2 in L or v1 = v2 or not v1,v2 are_c=-comparable )
then A2: ex w1 being Element of W st
( v1 = w1 & len w1 = n ) by A1;
assume v2 in L ; :: thesis: ( v1 = v2 or not v1,v2 are_c=-comparable )
then ex w2 being Element of W st
( v2 = w2 & len w2 = n ) by A1;
hence ( v1 = v2 or not v1,v2 are_c=-comparable ) by A2, TREES_1:4; :: thesis: verum

end;

hence L is AntiChain_of_Prefixes of W by TREES_1:def 11; :: thesis: verum