( 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 \ 2 & b = 1 implies ( a "\/" b = 3 & a "/\" b = 0 ) )
assume that
A1: a = 3 \ 2 and
A2: b = 1 ; :: thesis: ( a "\/" b = 3 & a "/\" b = 0 )
Segm 1 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: 3 \ 2 c= z9 by A1, A6, YELLOW_1:3;

A9: now :: thesis: not z9 = 1

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

end;

A11: now :: thesis: not z9 = 2

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

end;

A13: 1 c= z9 by A2, A7, YELLOW_1:3;

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

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

end;

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

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

end;

z9 <> 0 by A13;
hence t <= z9 by A4, A14, A11, A16, A9, ENUMSET1:def 4; :: thesis: verum

end;

A18: 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
A19: a >= z9 and
A20: b >= z9 ; :: thesis: z9 <= z
A21: z9 c= 3 \ 2 by A1, A19, YELLOW_1:3;

A22: now :: thesis: not z9 = 1

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

end;

A23: z9 c= 1 by A2, A20, YELLOW_1:3;

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

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

end;

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

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

end;

A27: now :: thesis: not z9 = 3

assume z9 = 3 ; :: thesis: contradiction
then 2 in z9 by CARD_1:51, ENUMSET1:def 1;
hence contradiction by A23, CARD_1:49, TARSKI:def 1; :: 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 A21, TARSKI:def 1, YELLOW11:4; :: thesis: verum

end;

hence z9 <= z by A4, A25, A24, A22, A27, 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, A18, YELLOW_0:22, YELLOW_0:23; :: thesis: verum