( 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

d <= z

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

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

A18:
for d being Element of B_6 st a >= d & b >= d holds
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;

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

end;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;assume z9 = 1 ; :: thesis: contradiction

hence contradiction by A8, A10, CARD_1:49, TARSKI:def 1; :: thesis: verum

A11: now :: thesis: not z9 = 2

A13:
1 c= z9
by A2, A7, YELLOW_1:3;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;then A12: not 2 in z9 ;

2 in 3 \ 2 by TARSKI:def 1, YELLOW11:4;

hence contradiction by A8, A12; :: thesis: verum

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;assume z9 = 3 \ 2 ; :: thesis: contradiction

hence contradiction by A13, A15, TARSKI:def 1, YELLOW11:4; :: thesis: verum

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

z9 <> 0
by A13;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;assume z9 = 3 \ 1 ; :: thesis: contradiction

hence contradiction by A13, A17, TARSKI:def 2, YELLOW11:3; :: thesis: verum

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

d <= z

proof

z c= b
;
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;

end;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

A23:
z9 c= 1
by A2, A20, YELLOW_1:3;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;then 0 in z9 by CARD_1:49, TARSKI:def 1;

hence contradiction by A21, TARSKI:def 1, YELLOW11:4; :: thesis: verum

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;then 2 in z9 by TARSKI:def 1, YELLOW11:4;

hence contradiction by A23, CARD_1:49, TARSKI:def 1; :: thesis: verum

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

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;then 2 in z9 by CARD_1:51, ENUMSET1:def 1;

hence contradiction by A23, CARD_1:49, TARSKI:def 1; :: thesis: verum

now :: thesis: not z9 = 2

hence
z9 <= z
by A4, A25, A24, A22, A27, ENUMSET1:def 4; :: thesis: verumassume
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;then 0 in z9 by CARD_1:50, TARSKI:def 2;

hence contradiction by A21, TARSKI:def 1, YELLOW11:4; :: thesis: verum

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