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 :: thesis: ( b is-lower-neighbour-of a & c is-lower-neighbour-of a implies b "\/" c = a )
assume that
A3: b is-lower-neighbour-of a and
A4: c is-lower-neighbour-of a ; :: thesis: b "\/" c = a
A5: b [= a by A3;
A6: c [= a by A4;
A7: 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 A3, A6;
hence contradiction by A1, A4; :: thesis: verum
end;
a = a "\/" a
.= (b "\/" a) "\/" a by A5, LATTICES:def 3
.= (b "\/" a) "\/" (c "\/" a) by A6, LATTICES:def 3
.= b "\/" (a "\/" (a "\/" c)) by LATTICES:def 5
.= b "\/" ((a "\/" a) "\/" c) by LATTICES:def 5
.= b "\/" (a "\/" c)
.= (b "\/" c) "\/" a by LATTICES:def 5 ;
then A8: b "\/" c [= a by LATTICES:def 3;
c [= b "\/" c by LATTICES:5;
hence b "\/" c = a by A4, A8, A7; :: thesis: verum
end;
now :: thesis: ( b is-upper-neighbour-of a & c is-upper-neighbour-of a implies b "/\" c = a )
assume that
A9: b is-upper-neighbour-of a and
A10: c is-upper-neighbour-of a ; :: thesis: b "/\" c = a
A11: a [= b by A9;
A12: a [= c by A10;
A13: not b "/\" c = c
proof
assume b "/\" c = c ; :: thesis: contradiction
then c [= b by LATTICES:4;
then ( c = a or c = b ) by A9, A12;
hence contradiction by A1, A10; :: thesis: verum
end;
a = a "/\" a
.= (b "/\" a) "/\" a by A11, LATTICES:4
.= (b "/\" a) "/\" (c "/\" a) by A12, LATTICES:4
.= b "/\" (a "/\" (c "/\" a)) by LATTICES:def 7
.= b "/\" ((a "/\" a) "/\" c) by LATTICES:def 7
.= b "/\" (a "/\" c)
.= (b "/\" c) "/\" a by LATTICES:def 7 ;
then A14: a [= b "/\" c by LATTICES:4;
b "/\" c [= c by LATTICES:6;
hence b "/\" c = a by A10, A14, A13; :: 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