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;
A2: 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 13 :: 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 A3: x in L ; :: thesis: x is FinSequence
A4: x is Element of W by A3;
thus x is FinSequence by A4; :: 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 A5: v1 in L ; :: thesis: ( not v2 in L or v1 = v2 or not v1,v2 are_c=-comparable )
A6: ex w1 being Element of W st
( v1 = w1 & len w1 = n ) by A1, A5;
assume A7: v2 in L ; :: thesis: ( v1 = v2 or not v1,v2 are_c=-comparable )
A8: ex w2 being Element of W st
( v2 = w2 & len w2 = n ) by A1, A7;
thus ( v1 = v2 or not v1,v2 are_c=-comparable ) by A6, A8, TREES_1:19; :: thesis: verum

end;

thus L is AntiChain_of_Prefixes of W by A2, TREES_1:def 14; :: thesis: verum