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, Def4;
then (X "\/" Y) "/\" (X "\/" (X `)) = X "\/" (Bottom L) by LATTICES:31;
then (X "\/" Y) "/\" (Top L) = X "\/" (Bottom L) by LATTICES:48
.= X by LATTICES:39 ;
then Y "\/" X = X by LATTICES:43;
then (Y "/\" X) ` [= Y ` by LATTICES:def 9;
then A5: X "\/" Y [= Y ` by A1, LATTICES:50;
A6: X "/\" (Y `) = Bottom L by A3, Def4;
then (Y "\/" X) "/\" (Y "\/" (Y `)) = Y "\/" (Bottom L) by LATTICES:31;
then (Y "\/" X) "/\" (Top L) = Y "\/" (Bottom L) by LATTICES:48
.= Y by LATTICES:39 ;
then X "\/" Y = Y by LATTICES:43;
then (X "/\" Y) ` [= X ` by LATTICES:def 9;
then A7: X "\/" Y [= X ` by A1, LATTICES:50;
((Y `) "\/" Y) "/\" ((Y `) "\/" (X `)) = (Y `) "\/" (Bottom L) by A4, LATTICES:31;
then (Top L) "/\" ((Y `) "\/" (X `)) = (Y `) "\/" (Bottom L) by LATTICES:48
.= Y ` by LATTICES:39 ;
then (X `) "\/" (Y `) = Y ` by LATTICES:43;
then ((X `) "/\" (Y `)) ` [= (X `) ` by LATTICES:def 9;
then ((X `) "/\" (Y `)) ` [= X by LATTICES:49;
then ((X `) `) "\/" ((Y `) `) [= X by LATTICES:50;
then X "\/" ((Y `) `) [= X by LATTICES:49;
then A8: (X `) "\/" (Y `) [= X by A1, LATTICES:49;
X ` [= (X `) "\/" (Y `) by LATTICES:22;
then A9: X ` [= X by A8, LATTICES:25;
((X `) "\/" X) "/\" ((X `) "\/" (Y `)) = (X `) "\/" (Bottom L) by A6, LATTICES:31;
then (Top L) "/\" ((X `) "\/" (Y `)) = (X `) "\/" (Bottom L) by LATTICES:48
.= X ` by LATTICES:39 ;
then (Y `) "\/" (X `) = X ` by LATTICES:43;
then ((Y `) "/\" (X `)) ` [= (Y `) ` by LATTICES:def 9;
then ((Y `) `) "\/" ((X `) `) [= (Y `) ` by LATTICES:50;
then ((Y `) `) "\/" ((X `) `) [= Y by LATTICES:49;
then ((Y `) `) "\/" X [= Y by LATTICES:49;
then A10: (X `) "\/" (Y `) [= Y by A1, LATTICES:49;
Y ` [= (X `) "\/" (Y `) by LATTICES:22;
then A11: Y ` [= Y by A10, LATTICES:25;
X [= X "\/" Y by LATTICES:22;
then A12: X [= X ` by A7, LATTICES:25;
Y [= X "\/" Y by LATTICES:22;
then Y [= Y ` by A5, LATTICES:25;
hence ( X = X ` & Y = Y ` ) by A11, A9, A12, Def3; :: thesis: verum