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 ) )
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 ) );
A1: % (~ ((d %) ~)) = ~ ((d %) ~) by LATTICE3:def 4
.= (d %) ~ by LATTICE3:def 7
.= d % by LATTICE3:def 6
.= 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]
( % (~ x) [= a & a <> % (~ x) implies ex c being Element of L st
( % (~ x) [= c & c is-lower-neighbour-of a ) )

proof

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

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

end;

end;

end;

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

end;

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