A1: the carrier of B_6 = {0,1,(3 \ 1),2,(3 \ 2),3} by YELLOW_1:1;
then reconsider z = 3 as Element of B_6 by ENUMSET1:def 4;
A2: Segm 2 c= Segm 3 by NAT_1:39;
let x, y be Element of B_6; :: thesis: ( x = 3 \ 2 & y = 2 implies ( x "\/" y = 3 & x "/\" y = 0 ) )
assume that
A3: x = 3 \ 2 and
A4: y = 2 ; :: thesis: ( x "\/" y = 3 & x "/\" y = 0 )
A5: 2 \/ (3 \ 2) = 2 \/ 3 by XBOOLE_1:39
.= 3 by A2, XBOOLE_1:12 ;
now :: thesis: ( x <= z & y <= z & ( for w being Element of B_6 st x <= w & y <= w holds
z <= w ) )
thus ( x <= z & y <= z ) by A3, YELLOW_1:3, A2, A4; :: 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 A3, A4, A5, 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 A1, ENUMSET1:def 4;
x misses y by A3, A4, XBOOLE_1:79;
then A6: x /\ y = 0 by XBOOLE_0:def 7;
now :: thesis: ( z <= x & z <= y & ( for w being Element of B_6 st w <= x & w <= y holds
w <= z ) )
( z c= x & z c= y ) ;
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 A6; :: thesis: verum
end;
hence x "/\" y = 0 by YELLOW_0:23; :: thesis: verum