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