let x, y be Element of B_6 ; :: thesis: ( x = 3 \ 2 & y = 2 implies ( x "\/" y = 3 & x "/\" y = 0 ) )
Z1: the carrier of B_6 = {0 ,1,(3 \ 1),2,(3 \ 2),3} by YELLOW_1:1;
assume Z: ( x = 3 \ 2 & y = 2 ) ; :: thesis: ( x "\/" y = 3 & x "/\" y = 0 )
x misses y by Z, XBOOLE_1:79;
then P: x /\ y = 0 by XBOOLE_0:def 7;
B: 2 c= 3 by NAT_1:40;
C: 2 \/ (3 \ 2) = 2 \/ 3 by XBOOLE_1:39
.= 3 by B, XBOOLE_1:12 ;
reconsider z = 3 as Element of B_6 by Z1, ENUMSET1:def 4;

now

( x c= z & y c= z ) by Z, NAT_1:40;
hence ( x <= z & y <= z ) by YELLOW_1:3; :: thesis: for w being Element of B_6 st x <= w & y <= w holds
z <= w
let w be Element of B_6 ; :: thesis: ( x <= w & y <= w implies z <= w )
assume ( x <= w & y <= w ) ; :: thesis: z <= w
then ( x c= w & y c= w ) by YELLOW_1:3;
then x \/ y c= w by XBOOLE_1:8;
hence z <= w by C, Z, YELLOW_1:3; :: thesis: verum

end;

hence x "\/" y = 3 by YELLOW_0:22; :: thesis: x "/\" y = 0
reconsider z = 0 as Element of B_6 by Z1, ENUMSET1:def 4;

now

( z c= x & z c= y ) by XBOOLE_1:2;
hence ( z <= x & z <= y ) by YELLOW_1:3; :: thesis: for w being Element of B_6 st w <= x & w <= y holds
w <= z
let w be Element of B_6 ; :: thesis: ( w <= x & w <= y implies w <= z )
assume ( w <= x & w <= y ) ; :: thesis: w <= z
then ( w c= x & w c= y ) by YELLOW_1:3;
then w c= x /\ y by XBOOLE_1:19;
hence w <= z by P; :: thesis: verum

end;

hence x "/\" y = 0 by YELLOW_0:23; :: thesis: verum