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 A2, XBOOLE_1:12 ;

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;

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 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 ) )

hence
x "\/" y = 3
by YELLOW_0:22; :: thesis: x "/\" y = 0 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;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

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 ) )

hence
x "/\" y = 0
by YELLOW_0:23; :: thesis: verumw <= 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 ( 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