let a, b be Element of Benzene; :: thesis: ( a = 3 \ 1 & b = 2 implies ( a "\/" b = 3 & a "/\" b = 0 ) )

assume A1: ( a = 3 \ 1 & b = 2 ) ; :: thesis: ( a "\/" b = 3 & a "/\" b = 0 )

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 A1, Th15;

hence ( a "\/" b = 3 & a "/\" b = 0 ) by Th14; :: thesis: verum

assume A1: ( a = 3 \ 1 & b = 2 ) ; :: thesis: ( a "\/" b = 3 & a "/\" b = 0 )

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 A1, Th15;

hence ( a "\/" b = 3 & a "/\" b = 0 ) by Th14; :: thesis: verum