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

proof

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

per cases ( ( a = 0 & b = 2 ) or ( a = 2 & b = 0 ) or ( not ( a = 0 & b = 2 ) & not ( a = 2 & b = 0 ) ) ) ;

suppose B1: ( a = 0 & b = 2 ) ; :: thesis: a "/\" (a "\/" b) = a

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

end;

suppose B1: ( a = 2 & b = 0 ) ; :: thesis: a "/\" (a "\/" b) = a

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

end;

suppose B1: ( not ( a = 0 & b = 2 ) & not ( a = 2 & b = 0 ) ) ; :: 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 ex123"\/" bb by EXUDef
.= aa by B1, UPDef, E ;
WW: ( not ( a = 0 & a = 2 ) & not ( a = 2 & a = 0 ) ) ;
a "/\" (a "\/" b) = aa ex123"/\" 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 ex123"\/" bb by EXUDef
.= bb by E, B1, UPDef ;
a "/\" (a "\/" b) = aa ex123"/\" 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 ExNearLattice is join-absorbing by LATTICES:def 9; :: thesis: verum