let L be Lattice; :: thesis: for a, b, c being Element of L st b <> c holds
( ( b is-upper-neighbour-of a & c is-upper-neighbour-of a implies a = c "/\" b ) & ( b is-lower-neighbour-of a & c is-lower-neighbour-of a implies a = c "\/" b ) )
let a be Element of L; :: thesis: for b, c being Element of L st b <> c holds
( ( b is-upper-neighbour-of a & c is-upper-neighbour-of a implies a = c "/\" b ) & ( b is-lower-neighbour-of a & c is-lower-neighbour-of a implies a = c "\/" b ) )
let b, c be Element of L; :: thesis: ( b <> c implies ( ( b is-upper-neighbour-of a & c is-upper-neighbour-of a implies a = c "/\" b ) & ( b is-lower-neighbour-of a & c is-lower-neighbour-of a implies a = c "\/" b ) ) )
assume A1: b <> c ; :: thesis: ( ( b is-upper-neighbour-of a & c is-upper-neighbour-of a implies a = c "/\" b ) & ( b is-lower-neighbour-of a & c is-lower-neighbour-of a implies a = c "\/" b ) )

A2: now

assume A3: ( b is-upper-neighbour-of a & c is-upper-neighbour-of a ) ; :: thesis: b "/\" c = a
then A4: ( a [= b & a [= c ) by Def5;
a = a "/\" a by LATTICES:18
.= (b "/\" a) "/\" a by A4, LATTICES:21
.= (b "/\" a) "/\" (c "/\" a) by A4, LATTICES:21
.= b "/\" (a "/\" (c "/\" a)) by LATTICES:def 7
.= b "/\" ((a "/\" a) "/\" c) by LATTICES:def 7
.= b "/\" (a "/\" c) by LATTICES:18
.= (b "/\" c) "/\" a by LATTICES:def 7 ;
then A5: a [= b "/\" c by LATTICES:21;
A6: b "/\" c [= c by LATTICES:23;
not b "/\" c = c

proof

assume b "/\" c = c ; :: thesis: contradiction
then c [= b by LATTICES:21;
then ( c = a or c = b ) by A3, A4, Def5;
hence contradiction by A1, A3, Def5; :: thesis: verum

end;

hence b "/\" c = a by A3, A5, A6, Def5; :: thesis: verum

end;

now

assume A7: ( b is-lower-neighbour-of a & c is-lower-neighbour-of a ) ; :: thesis: b "\/" c = a
then A8: ( b [= a & c [= a ) by Def5;
a = a "\/" a by LATTICES:17
.= (b "\/" a) "\/" a by A8, LATTICES:def 3
.= (b "\/" a) "\/" (c "\/" a) by A8, LATTICES:def 3
.= b "\/" (a "\/" (a "\/" c)) by LATTICES:def 5
.= b "\/" ((a "\/" a) "\/" c) by LATTICES:def 5
.= b "\/" (a "\/" c) by LATTICES:17
.= (b "\/" c) "\/" a by LATTICES:def 5 ;
then A9: b "\/" c [= a by LATTICES:def 3;
A10: c [= b "\/" c by LATTICES:22;
not b "\/" c = c

proof

assume b "\/" c = c ; :: thesis: contradiction
then b [= c by LATTICES:def 3;
then ( c = a or c = b ) by A7, A8, Def5;
hence contradiction by A1, A7, Def5; :: thesis: verum

end;

hence b "\/" c = a by A7, A9, A10, Def5; :: thesis: verum

end;

hence ( ( b is-upper-neighbour-of a & c is-upper-neighbour-of a implies a = c "/\" b ) & ( b is-lower-neighbour-of a & c is-lower-neighbour-of a implies a = c "\/" b ) ) by A2; :: thesis: verum