let L be B_Lattice; for X, Y being Element of L st (X `) "\/" (Y `) = X "\/" Y & Y misses X ` & X misses Y ` holds
( X = X ` & Y = Y ` )
let X, Y be Element of L; ( (X `) "\/" (Y `) = X "\/" Y & Y misses X ` & X misses Y ` implies ( X = X ` & Y = Y ` ) )
assume that
A1:
(X `) "\/" (Y `) = X "\/" Y
and
A2:
Y misses X `
and
A3:
X misses Y `
; ( X = X ` & Y = Y ` )
A4:
Y "/\" (X `) = Bottom L
by A2;
then
(X "\/" Y) "/\" (X "\/" (X `)) = X "\/" (Bottom L)
by LATTICES:11;
then
(X "\/" Y) "/\" (Top L) = X
by LATTICES:21;
then
(Y "/\" X) ` [= Y `
by LATTICES:def 9;
then A5:
X "\/" Y [= Y `
by A1, LATTICES:23;
A6:
X "/\" (Y `) = Bottom L
by A3;
then
(Y "\/" X) "/\" (Y "\/" (Y `)) = Y "\/" (Bottom L)
by LATTICES:11;
then
(Y "\/" X) "/\" (Top L) = Y
by LATTICES:21;
then
(X "/\" Y) ` [= X `
by LATTICES:def 9;
then A7:
X "\/" Y [= X `
by A1, LATTICES:23;
((Y `) "\/" Y) "/\" ((Y `) "\/" (X `)) = (Y `) "\/" (Bottom L)
by A4, LATTICES:11;
then
(Top L) "/\" ((Y `) "\/" (X `)) = Y `
by LATTICES:21;
then
((X `) "/\" (Y `)) ` [= (X `) `
by LATTICES:def 9;
then
((X `) "/\" (Y `)) ` [= X
;
then
((X `) `) "\/" ((Y `) `) [= X
by LATTICES:23;
then
X "\/" ((Y `) `) [= X
;
then A8:
(X `) "\/" (Y `) [= X
by A1;
X ` [= (X `) "\/" (Y `)
by LATTICES:5;
then A9:
X ` [= X
by A8, LATTICES:7;
((X `) "\/" X) "/\" ((X `) "\/" (Y `)) = (X `) "\/" (Bottom L)
by A6, LATTICES:11;
then
(Top L) "/\" ((X `) "\/" (Y `)) = X `
by LATTICES:21;
then
((Y `) "/\" (X `)) ` [= (Y `) `
by LATTICES:def 9;
then
((Y `) `) "\/" ((X `) `) [= (Y `) `
by LATTICES:23;
then
((Y `) `) "\/" ((X `) `) [= Y
;
then
((Y `) `) "\/" X [= Y
;
then A10:
(X `) "\/" (Y `) [= Y
by A1;
Y ` [= (X `) "\/" (Y `)
by LATTICES:5;
then A11:
Y ` [= Y
by A10, LATTICES:7;
X [= X "\/" Y
by LATTICES:5;
then A12:
X [= X `
by A7, LATTICES:7;
Y [= X "\/" Y
by LATTICES:5;
then
Y [= Y `
by A5, LATTICES:7;
hence
( X = X ` & Y = Y ` )
by A11, A9, A12; verum