( 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 ;
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 ;
A9: now :: thesis: not z9 = 3 \ 1end;
A11: 3 \ 1 c= z9 by ;
A12: now :: thesis: not z9 = 2
assume z9 = 2 ; :: thesis: contradiction
then A13: not 2 in z9 ;
2 in 3 \ 1 by ;
hence contradiction by A11, A13; :: thesis: verum
end;
A14: now :: thesis: not z9 = 3 \ 2end;
( 1 in 2 & 0 in 2 ) by ;
then ( 1 in z9 & 0 in z9 ) by A8;
then ( z9 <> 1 & z9 <> 0 ) ;
hence t <= z9 by ; :: 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 ;
A20: now :: thesis: not z9 = 1end;
A21: z9 c= 2 by ;
A22: now :: thesis: not z9 = 3 \ 1
assume z9 = 3 \ 1 ; :: thesis: contradiction
then A23: 2 in z9 by ;
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 ;
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 ;
not 2 in 2 ;
hence contradiction by A21, A27; :: thesis: verum
end;
now :: thesis: not z9 = 2end;
hence z9 <= z by ; :: 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 ;
hence ( a "\/" b = 3 & a "/\" b = 0 ) by ; :: thesis: verum