let W be Tree; :: thesis: for w being Element of W holds succ w is AntiChain_of_Prefixes of W
let w be Element of W; :: thesis: succ w is AntiChain_of_Prefixes of W
succ w is AntiChain_of_Prefixes-like

proof

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

proof

let x be set ; :: thesis: ( x in succ w implies x is FinSequence )
assume x in succ w ; :: thesis: x is FinSequence
then ex i being Element of NAT st
( x = w ^ <*i*> & w ^ <*i*> in W ) ;
hence x is FinSequence ; :: thesis: verum

end;

let v1, v2 be FinSequence; :: thesis: ( not v1 in succ w or not v2 in succ w or v1 = v2 or not v1,v2 are_c=-comparable )
assume v1 in succ w ; :: thesis: ( not v2 in succ w or v1 = v2 or not v1,v2 are_c=-comparable )
then A5: ex k1 being Element of NAT st
( v1 = w ^ <*k1*> & w ^ <*k1*> in W ) ;
assume v2 in succ w ; :: thesis: ( v1 = v2 or not v1,v2 are_c=-comparable )
then A7: ex k2 being Element of NAT st
( v2 = w ^ <*k2*> & w ^ <*k2*> in W ) ;
A8: len v1 = (len w) + 1 by A5, FINSEQ_2:19;
len v2 = (len w) + 1 by A7, FINSEQ_2:19;
hence ( v1 = v2 or not v1,v2 are_c=-comparable ) by A8, TREES_1:19; :: thesis: verum

end;

hence succ w is AntiChain_of_Prefixes of W by TREES_1:def 14; :: thesis: verum