let L be co-noetherian Lattice; :: thesis: for a, d being Element of L st d [= a & a <> d holds
ex c being Element of L st
( d [= c & c is-lower-neighbour-of a )
let a, d be Element of L; :: thesis: ( d [= a & a <> d implies ex c being Element of L st
( d [= c & c is-lower-neighbour-of a ) )
assume A1: ( d [= a & a <> d ) ; :: thesis: ex c being Element of L st
( d [= c & c is-lower-neighbour-of a )
defpred S₁[ Element of ((LattPOSet L) ~ )] means ( % (~ $1) [= a & a <> % (~ $1) implies ex c being Element of L st
( % (~ $1) [= c & c is-lower-neighbour-of a ) );
A2: (LattPOSet L) ~ is well_founded by Def4;
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]
( % (~ x) [= a & a <> % (~ x) implies ex c being Element of L st
( % (~ x) [= c & c is-lower-neighbour-of a ) )

proof

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

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

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

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

end;

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

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

end;

end;

end;

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

end;

A11: 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 7
.= d % by LATTICE3:def 6
.= d by LATTICE3:def 3 ;
hence ex c being Element of L st
( d [= c & c is-lower-neighbour-of a ) by A1, A11; :: thesis: verum