theorem Th17: :: ROBBINS4:17
for a, b being Element of B_6 st a = 3 \ 1 & b = 1 holds
( a "\/" b = 3 & a "/\" b = 0 )