let a, b be Element of ExWALattice; :: thesis: ( a = 1 & b = 2 implies a "/\" b = 1 )
reconsider aa = a, bb = b as Element of {0,1,2,3,4} ;
assume A1: ( a = 1 & b = 2 ) ; :: thesis: a "/\" b = 1
a "/\" b = aa ex1234"/\" bb by EXNDef
.= min (aa,bb) by A1, ExMeetDef ;
hence a "/\" b = 1 by A1, XXREAL_0:def 9; :: thesis: verum