let a, b be Element of Benzene ; :: thesis: ( a = 3 \ 2 & b = 1 implies a "\/" b = 3 )
assume A: ( a = 3 \ 2 & b = 1 ) ; :: thesis: a "\/" b = 3
then ( a in {0 ,1,(3 \ 1),2,(3 \ 2),3} & b in {0 ,1,(3 \ 1),2,(3 \ 2),3} ) by ENUMSET1:def 4;
then reconsider aa = a, bb = b as Element of B_6 by YELLOW_1:1;
( aa "\/" bb = 3 & aa "/\" bb = 0 ) by A, Ha11;
hence a "\/" b = 3 by Ha0; :: thesis: verum