let L be B_Lattice; :: thesis: 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; :: thesis: ( (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 ` ; :: thesis: ( 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; :: thesis: verum