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