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 1 c= Segm 3 by NAT_1:39;
let x, y be Element of B_6; :: thesis: ( x = 3 \ 1 & y = 1 implies ( x "\/" y = 3 & x "/\" y = 0 ) )
assume that
A3: x = 3 \ 1 and
A4: y = 1 ; :: thesis: ( x "\/" y = 3 & x "/\" y = 0 )
A5: 1 \/ (3 \ 1) = 1 \/ 3 by XBOOLE_1:39
.= 3 by ;
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 ; :: 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 ; :: thesis: verum
end;
hence x "\/" y = 3 by YELLOW_0:22; :: thesis: x "/\" y = 0
reconsider z = 0 as Element of B_6 by ;
x misses y by ;
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