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 10 :: thesis: for b1, b2 being set holds
( not b1 in succ w or not b2 in succ w or b1 = b2 or not b1,b2 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 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 A1: ex k1 being 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 A2: ex k2 being Nat st
( v2 = w ^ <*k2*> & w ^ <*k2*> in W ) ;
A3: len v1 = (len w) + 1 by A1, FINSEQ_2:16;
len v2 = (len w) + 1 by A2, FINSEQ_2:16;
hence ( v1 = v2 or not v1,v2 are_c=-comparable ) by A3, TREES_1:4; :: thesis: verum
end;
hence succ w is AntiChain_of_Prefixes of W by TREES_1:def 11; :: thesis: verum