let a, b be Element of B_6 ; :: thesis: ( a = 3 \ 2 & b = 1 implies ( a "\/" b = 3 & a "/\" b = 0 ) )
Z1: the carrier of B_6 = {0 ,1,(3 \ 1),2,(3 \ 2),3} by YELLOW_1:1;
assume Z: ( a = 3 \ 2 & b = 1 ) ; :: thesis: ( a "\/" b = 3 & a "/\" b = 0 )
( 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;
( a c= t & b c= t ) by Z, NAT_1:40;
then A0: ( a <= t & b <= t ) by YELLOW_1:3;
a1: for d being Element of B_6 st d >= a & d >= b holds
t <= d
proof
let z' be Element of B_6 ; :: thesis: ( z' >= a & z' >= b implies t <= z' )
assume ( z' >= a & z' >= b ) ; :: thesis: t <= z'
then A11: ( 3 \ 2 c= z' & 1 c= z' ) by Z, YELLOW_1:3;
A12: now
assume z' = 3 \ 2 ; :: thesis: contradiction
then ( not 0 in z' & 0 in 1 ) by CARD_1:87, TARSKI:def 1, YELLOW11:4;
hence contradiction by A11; :: thesis: verum
end;
A13: now
assume z' = 2 ; :: thesis: contradiction
then ( not 2 in z' & 2 in 3 \ 2 ) by TARSKI:def 1, YELLOW11:4;
hence contradiction by A11; :: thesis: verum
end;
A14: now
assume z' = 3 \ 1 ; :: thesis: contradiction
then ( not 0 in z' & 0 in 1 ) by CARD_1:87, TARSKI:def 1, TARSKI:def 2, YELLOW11:3;
hence contradiction by A11; :: thesis: verum
end;
A00: now
assume z' = 1 ; :: thesis: contradiction
then ( 2 in 3 \ 2 & not 2 in z' ) by CARD_1:87, TARSKI:def 1, YELLOW11:4;
hence contradiction by A11; :: thesis: verum
end;
z' <> 0 by A11;
hence t <= z' by A00, A12, A13, A14, Z1, ENUMSET1:def 4; :: thesis: verum
end;
( z c= a & z c= b ) by XBOOLE_1:2;
then Z0: ( z <= a & z <= b ) by YELLOW_1:3;
for d being Element of B_6 st a >= d & b >= d holds
d <= z
proof
let z' be Element of B_6 ; :: thesis: ( a >= z' & b >= z' implies z' <= z )
assume ( a >= z' & b >= z' ) ; :: thesis: z' <= z
then A11: ( z' c= 3 \ 2 & z' c= 1 ) by Z, YELLOW_1:3;
A12: now
assume z' = 3 \ 1 ; :: thesis: contradiction
then ( 2 in z' & not 2 in 1 ) by CARD_1:88, TARSKI:def 2, YELLOW11:3;
hence contradiction by A11; :: thesis: verum
end;
A13: now
assume z' = 2 ; :: thesis: contradiction
then ( 0 in z' & not 0 in 3 \ 2 ) by CARD_1:88, TARSKI:def 1, TARSKI:def 2, YELLOW11:4;
hence contradiction by A11; :: thesis: verum
end;
A14: now
assume z' = 3 \ 2 ; :: thesis: contradiction
then ( 2 in z' & not 2 in 1 ) by CARD_1:87, TARSKI:def 1, YELLOW11:4;
hence contradiction by A11; :: thesis: verum
end;
A00: now
assume z' = 1 ; :: thesis: contradiction
then ( 0 in z' & not 0 in 3 \ 2 ) by CARD_1:87, TARSKI:def 1, YELLOW11:4;
hence contradiction by A11; :: thesis: verum
end;
now
assume z' = 3 ; :: thesis: contradiction
then ( 2 in z' & not 2 in 1 ) by CARD_1:87, CARD_1:89, ENUMSET1:def 1, TARSKI:def 1;
hence contradiction by A11; :: thesis: verum
end;
hence z' <= z by A00, A12, A13, A14, Z1, ENUMSET1:def 4; :: thesis: verum
end;
hence ( a "\/" b = 3 & a "/\" b = 0 ) by a1, Z0, A0, YELLOW_0:22, YELLOW_0:23; :: thesis: verum