( 3 in {0,1,(3 \ 1),2,(3 \ 2),3} & 0 in {0,1,(3 \ 1),2,(3 \ 2),3} ) by ENUMSET1:def 4;
then reconsider t = 3, z = 0 as Element of B_6 by YELLOW_1:1;
let a, b be Element of B_6; :: thesis: ( a = 3 \ 1 & b = 2 implies ( a "\/" b = 3 & a "/\" b = 0 ) )
assume that
A1: a = 3 \ 1 and
A2: b = 2 ; :: thesis: ( a "\/" b = 3 & a "/\" b = 0 )
Segm 2 c= Segm 3 by NAT_1:39;
then A3: b <= t by YELLOW_1:3, A2;
A4: the carrier of B_6 = {0,1,(3 \ 1),2,(3 \ 2),3} by YELLOW_1:1;
A5: for d being Element of B_6 st d >= a & d >= b holds
t <= d

proof

let z9 be Element of B_6; :: thesis: ( z9 >= a & z9 >= b implies t <= z9 )
assume that
A6: z9 >= a and
A7: z9 >= b ; :: thesis: t <= z9
A8: Segm 2 c= z9 by A2, A7, YELLOW_1:3;

A9: now :: thesis: not z9 = 3 \ 1

A10: 0 in 2 by CARD_1:50, TARSKI:def 2;
assume z9 = 3 \ 1 ; :: thesis: contradiction
hence contradiction by A8, A10, TARSKI:def 2, YELLOW11:3; :: thesis: verum

end;

A11: 3 \ 1 c= z9 by A1, A6, YELLOW_1:3;

A12: now :: thesis: not z9 = 2

assume z9 = 2 ; :: thesis: contradiction
then A13: not 2 in z9 ;
2 in 3 \ 1 by TARSKI:def 2, YELLOW11:3;
hence contradiction by A11, A13; :: thesis: verum

end;

A14: now :: thesis: not z9 = 3 \ 2

A15: 1 in 2 by CARD_1:50, TARSKI:def 2;
assume z9 = 3 \ 2 ; :: thesis: contradiction
hence contradiction by A8, A15, TARSKI:def 1, YELLOW11:4; :: thesis: verum

end;

( 1 in 2 & 0 in 2 ) by TARSKI:def 2, CARD_1:50;
then ( 1 in z9 & 0 in z9 ) by A8;
then ( z9 <> 1 & z9 <> 0 ) ;
hence t <= z9 by A4, A9, A12, A14, ENUMSET1:def 4; :: thesis: verum

end;

A16: for d being Element of B_6 st a >= d & b >= d holds
d <= z

proof

let z9 be Element of B_6; :: thesis: ( a >= z9 & b >= z9 implies z9 <= z )
assume that
A17: a >= z9 and
A18: b >= z9 ; :: thesis: z9 <= z
A19: z9 c= 3 \ 1 by A1, A17, YELLOW_1:3;

A20: now :: thesis: not z9 = 1

assume z9 = 1 ; :: thesis: contradiction
then 0 in z9 by CARD_1:49, TARSKI:def 1;
hence contradiction by A19, TARSKI:def 2, YELLOW11:3; :: thesis: verum

end;

A21: z9 c= 2 by A2, A18, YELLOW_1:3;

A22: now :: thesis: not z9 = 3 \ 1

assume z9 = 3 \ 1 ; :: thesis: contradiction
then A23: 2 in z9 by TARSKI:def 2, YELLOW11:3;
not 2 in 2 ;
hence contradiction by A21, A23; :: thesis: verum

end;

A24: now :: thesis: not z9 = 3

assume z9 = 3 ; :: thesis: contradiction
then A25: 2 in z9 by CARD_1:51, ENUMSET1:def 1;
not 2 in 2 ;
hence contradiction by A21, A25; :: thesis: verum

end;

A26: now :: thesis: not z9 = 3 \ 2

assume z9 = 3 \ 2 ; :: thesis: contradiction
then A27: 2 in z9 by TARSKI:def 1, YELLOW11:4;
not 2 in 2 ;
hence contradiction by A21, A27; :: thesis: verum

end;

now :: thesis: not z9 = 2

assume z9 = 2 ; :: thesis: contradiction
then 0 in z9 by CARD_1:50, TARSKI:def 2;
hence contradiction by A19, TARSKI:def 2, YELLOW11:3; :: thesis: verum

end;

hence z9 <= z by A4, A22, A26, A20, A24, ENUMSET1:def 4; :: thesis: verum

end;

z c= b ;
then A28: z <= b by YELLOW_1:3;
z c= a ;
then A29: z <= a by YELLOW_1:3;
a <= t by A1, YELLOW_1:3;
hence ( a "\/" b = 3 & a "/\" b = 0 ) by A3, A5, A29, A28, A16, YELLOW_0:22, YELLOW_0:23; :: thesis: verum