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