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