let W be Tree; :: thesis: for A being AntiChain_of_Prefixes of W
for C being Chain of W ex w being Element of W st A /\ C c= {w}
let A be AntiChain_of_Prefixes of W; :: thesis: for C being Chain of W ex w being Element of W st A /\ C c= {w}
let C be Chain of W; :: thesis: ex w being Element of W st A /\ C c= {w}
A1: now :: thesis: for p, q being FinSequence of NAT st p in A /\ C & q in A /\ C holds
p = q
let p, q be FinSequence of NAT ; :: thesis: ( p in A /\ C & q in A /\ C implies p = q )
assume A2: ( p in A /\ C & q in A /\ C ) ; :: thesis: p = q
then A3: ( p in A & q in A ) by XBOOLE_0:def 4;
( p in C & q in C ) by A2, XBOOLE_0:def 4;
then p,q are_c=-comparable by Def3;
hence p = q by A3, TREES_1:def 10; :: thesis: verum
end;
set w = the Element of W;
now :: thesis: ex w being Element of W st A /\ C c= {w}
per cases ( A /\ C = {} or A /\ C <> {} ) ;
suppose A /\ C = {} ; :: thesis: ex w being Element of W st A /\ C c= {w}
then A /\ C c= { the Element of W} ;
hence ex w being Element of W st A /\ C c= {w} ; :: thesis: verum
end;
suppose A4: A /\ C <> {} ; :: thesis: ex x being Element of W st A /\ C c= {x}
set x = the Element of A /\ C;
the Element of A /\ C in C by A4, XBOOLE_0:def 4;
then reconsider x = the Element of A /\ C as Element of W ;
take x = x; :: thesis: A /\ C c= {x}
thus A /\ C c= {x} :: thesis: verum
proof
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in A /\ C or y in {x} )
assume A5: y in A /\ C ; :: thesis: y in {x}
then y is Element of W ;
then reconsider y9 = y as FinSequence of NAT ;
x = y9 by A1, A5;
hence y in {x} by TARSKI:def 1; :: thesis: verum
end;
end;
end;
end;
hence ex w being Element of W st A /\ C c= {w} ; :: thesis: verum