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

proof

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

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 "/\" b) "\/" b = b

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

end;

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

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

end;

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

per cases ( min (aa,bb) = aa or min (aa,bb) = bb ) by XXREAL_0:15;

suppose B2: min (aa,bb) = aa ; :: thesis: (a "/\" b) "\/" b = b

then (a "/\" b) "\/" b = a "\/" b by a0, B1, ExMeetDef
.= aa ex1234"\/" bb by EXUDef
.= max (aa,bb) by UPDef, B1
.= bb by B2, XXREAL_0:def 10, XXREAL_0:17 ;
hence (a "/\" b) "\/" b = b ; :: thesis: verum

end;

suppose B4: min (aa,bb) = bb ; :: thesis: (a "/\" b) "\/" b = b

A5: ( not ( b = 1 & b = 3 ) & not ( b = 3 & b = 1 ) ) ;
(a "/\" b) "\/" b = b "\/" b by B4, a0, B1, ExMeetDef
.= bb ex1234"\/" bb by EXUDef
.= max (bb,bb) by UPDef, A5
.= bb ;
hence (a "/\" b) "\/" b = b ; :: thesis: verum

end;

end;

end;

end;

end;

hence ExWALattice is meet-absorbing by LATTICES:def 8; :: thesis: verum