let a, b be Element of ExNearLattice; :: thesis: ( a = 1 & b = 2 implies a "\/" b = 2 )
reconsider aa = a, bb = b as Element of {0,1,2} by LATWAL_1:def 10;
assume A1: ( a = 1 & b = 2 ) ; :: thesis: a "\/" b = 2
a "\/" b = aa ex123"\/" bb by LATWAL_1:def 8, LATWAL_1:def 10
.= max (1,2) by A1, LATWAL_1:def 7
.= 2 by XXREAL_0:def 10 ;
hence a "\/" b = 2 ; :: thesis: verum