let a, b be Element of Benzene; ( a = 3 \ 1 & b = 1 implies a "\/" b = 3 )
assume A1:
( a = 3 \ 1 & b = 1 )
; 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
by A1, Th17;
hence
a "\/" b = 3
by Th14; verum