set L = ExWALattice ;
for a, b being Element of ExWALattice holds a "/\" (a "\/" b) = a

proof

let a, b be Element of ExWALattice; :: thesis: a "/\" (a "\/" b) = a
reconsider aa = a, bb = b as Element of {0,1,2,3,4} ;

per cases ( ( a = 1 & b = 3 ) or ( a = 3 & b = 1 ) or ( not ( a = 1 & b = 3 ) & not ( a = 3 & b = 1 ) ) ) ;

suppose B1: ( a = 1 & b = 3 ) ; :: thesis: a "/\" (a "\/" b) = a

then aa ex1234"\/" bb = aa by UPDef;
then a "/\" (a "\/" b) = a "/\" a by EXUDef
.= aa ex1234"/\" aa by EXNDef
.= min (aa,aa) by ExMeetDef, B1
.= aa ;
hence a "/\" (a "\/" b) = a ; :: thesis: verum

end;

suppose B1: ( a = 3 & b = 1 ) ; :: thesis: a "/\" (a "\/" b) = a

then aa ex1234"\/" bb = bb by UPDef;
then a "/\" (a "\/" b) = a "/\" b by EXUDef
.= aa ex1234"/\" bb by EXNDef
.= aa by ExMeetDef, B1 ;
hence a "/\" (a "\/" b) = a ; :: thesis: verum

end;

suppose B1: ( not ( a = 1 & b = 3 ) & not ( a = 3 & b = 1 ) ) ; :: thesis: a "/\" (a "\/" b) = a

per cases ( max (aa,bb) = aa or max (aa,bb) = bb ) by XXREAL_0:16;

suppose E: max (aa,bb) = aa ; :: thesis: a "/\" (a "\/" b) = a

A3: a "\/" b = aa ex1234"\/" bb by EXUDef
.= aa by B1, UPDef, E ;
WW: ( not ( a = 1 & a = 3 ) & not ( a = 3 & a = 1 ) ) ;
a "/\" (a "\/" b) = aa ex1234"/\" aa by EXNDef, A3
.= min (aa,aa) by ExMeetDef, WW
.= aa ;
hence a "/\" (a "\/" b) = a ; :: thesis: verum

end;

suppose E: max (aa,bb) = bb ; :: thesis: a "/\" (a "\/" b) = a

A3: a "\/" b = aa ex1234"\/" bb by EXUDef
.= bb by E, B1, UPDef ;
a "/\" (a "\/" b) = aa ex1234"/\" bb by EXNDef, A3
.= min (aa,bb) by ExMeetDef, B1
.= aa by E, XXREAL_0:def 9, XXREAL_0:25 ;
hence a "/\" (a "\/" b) = a ; :: thesis: verum

end;

end;

end;

end;

end;

hence ExWALattice is join-absorbing by LATTICES:def 9; :: thesis: verum