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 ) )
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 ) );
A1: % (d %) = d % by LATTICE3:def 4
.= d by LATTICE3:def 3 ;
A2: 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 A3: 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

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

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
A6: a [= c and
A7: c [= % x and
A8: ( not c = % x & not c = a ) by A5;
c % <= x by A4, A7, LATTICE3:7;
then A9: [(c %),x] in the InternalRel of (LattPOSet L) by ORDERS_2:def 5;
% (c %) = c % by LATTICE3:def 4
.= c by LATTICE3:def 3 ;
then ex c9 being Element of L st
( c9 [= c & c9 is-upper-neighbour-of a ) by A3, A6, A8, A9;
hence ex c being Element of L st
( c [= % x & c is-upper-neighbour-of a ) by A7, LATTICES:7; :: thesis: verum

end;

end;

end;

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

end;

A10: LattPOSet L is well_founded by Def3;
A11: for x being Element of (LattPOSet L) holds S₁[x] from WELLFND1:sch 3(A2, A10);
assume ( a [= d & a <> d ) ; :: thesis: ex c being Element of L st
( c [= d & c is-upper-neighbour-of a )
hence ex c being Element of L st
( c [= d & c is-upper-neighbour-of a ) by A11, A1; :: thesis: verum