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