( 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

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, A16, 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 \ 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

A16:
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: Segm 2 c= z9 by A2, A7, YELLOW_1:3;

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

A11:
3 \ 1 c= z9
by A1, A6, YELLOW_1:3;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;assume z9 = 3 \ 1 ; :: thesis: contradiction

hence contradiction by A8, A10, TARSKI:def 2, YELLOW11:3; :: thesis: verum

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;then A13: not 2 in z9 ;

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

hence contradiction by A11, A13; :: thesis: verum

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

( 1 in 2 & 0 in 2 )
by TARSKI:def 2, CARD_1:50;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;assume z9 = 3 \ 2 ; :: thesis: contradiction

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

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

d <= z

proof

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

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

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

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

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

not 2 in 2 ;

hence contradiction by A21, A23; :: thesis: verum

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

not 2 in 2 ;

hence contradiction by A21, A25; :: thesis: verum

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

not 2 in 2 ;

hence contradiction by A21, A27; :: thesis: verum

now :: thesis: not z9 = 2

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

hence contradiction by A19, TARSKI:def 2, YELLOW11:3; :: 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, A16, YELLOW_0:22, YELLOW_0:23; :: thesis: verum