let L be noetherian Lattice; :: thesis: for a, d being Element of L st a [= d & a <> d holds
ex c being Element of L st
( c [= d & c is-upper-neighbour-of a )
let a, d be Element of L; :: thesis: ( a [= d & a <> d implies ex c being Element of L st
( c [= d & c is-upper-neighbour-of a ) )
assume A1: ( a [= d & a <> d ) ; :: thesis: ex c being Element of L st
( c [= d & c is-upper-neighbour-of a )
defpred S₁[ Element of (LattPOSet L)] means ( a [= % $1 & a <> % $1 implies ex c being Element of L st
( c [= % $1 & c is-upper-neighbour-of a ) );
A2: LattPOSet L is well_founded by Def3;
A3: for x being Element of (LattPOSet L) st ( for y being Element of (LattPOSet L) st y <> x & [y,x] in the InternalRel of (LattPOSet L) holds
S₁[y] ) holds
S₁[x]

proof

let x be Element of (LattPOSet L); :: thesis: ( ( for y being Element of (LattPOSet L) st y <> x & [y,x] in the InternalRel of (LattPOSet L) holds
S₁[y] ) implies S₁[x] )
assume A4: for y being Element of (LattPOSet L) st y <> x & [y,x] in the InternalRel of (LattPOSet L) holds
S₁[y] ; :: thesis: S₁[x]
( a [= % x & a <> % x implies ex c being Element of L st
( c [= % x & c is-upper-neighbour-of a ) )

proof

assume A5: ( a [= % x & a <> % x ) ; :: thesis: ex c being Element of L st
( c [= % x & c is-upper-neighbour-of a )
A6: (% x) % = % x by LATTICE3:def 3
.= x by LATTICE3:def 4 ;

per cases ( % x is-upper-neighbour-of a or not % x is-upper-neighbour-of a ) ;

suppose % x is-upper-neighbour-of a ; :: thesis: ex c being Element of L st
( c [= % x & c is-upper-neighbour-of a )

hence ex c being Element of L st
( c [= % x & c is-upper-neighbour-of a ) ; :: thesis: verum

end;

suppose not % x is-upper-neighbour-of a ; :: thesis: ex c being Element of L st
( c [= % x & c is-upper-neighbour-of a )

then consider c being Element of L such that
A7: ( a [= c & c [= % x & not c = % x & not c = a ) by A5, Def5;
A8: % (c % ) = c % by LATTICE3:def 4
.= c by LATTICE3:def 3 ;
c % <= x by A6, A7, LATTICE3:7;
then [(c % ),x] in the InternalRel of (LattPOSet L) by ORDERS_2:def 9;
then consider c' being Element of L such that
A9: ( c' [= c & c' is-upper-neighbour-of a ) by A4, A7, A8;
thus ex c being Element of L st
( c [= % x & c is-upper-neighbour-of a ) by A7, A9, LATTICES:25; :: thesis: verum

end;

end;

end;

hence S₁[x] ; :: thesis: verum

end;

A10: for x being Element of (LattPOSet L) holds S₁[x] from WELLFND1:sch 3(A3, A2);
% (d % ) = d % by LATTICE3:def 4
.= d by LATTICE3:def 3 ;
hence ex c being Element of L st
( c [= d & c is-upper-neighbour-of a ) by A1, A10; :: thesis: verum