set N = B_6 ;

set Z = {0,1,(3 \ 1),2,(3 \ 2),3};

A1: the carrier of B_6 = {0,1,(3 \ 1),2,(3 \ 2),3} by YELLOW_1:1;

A2: B_6 is with_suprema

set Z = {0,1,(3 \ 1),2,(3 \ 2),3};

A1: the carrier of B_6 = {0,1,(3 \ 1),2,(3 \ 2),3} by YELLOW_1:1;

A2: B_6 is with_suprema

proof

B_6 is with_infima
let x, y be Element of B_6; :: according to LATTICE3:def 10 :: thesis: ex b_{1} being Element of the carrier of B_6 st

( x <= b_{1} & y <= b_{1} & ( for b_{2} being Element of the carrier of B_6 holds

( not x <= b_{2} or not y <= b_{2} or b_{1} <= b_{2} ) ) )

A3: {0,1,(3 \ 1),2,(3 \ 2),3} = the carrier of B_6 by YELLOW_1:1;

thus ex z being Element of B_6 st

( x <= z & y <= z & ( for z9 being Element of B_6 st x <= z9 & y <= z9 holds

z <= z9 ) ) :: thesis: verum

end;( x <= b

( not x <= b

A3: {0,1,(3 \ 1),2,(3 \ 2),3} = the carrier of B_6 by YELLOW_1:1;

thus ex z being Element of B_6 st

( x <= z & y <= z & ( for z9 being Element of B_6 st x <= z9 & y <= z9 holds

z <= z9 ) ) :: thesis: verum

proof
end;

per cases
( ( x = 0 & y = 0 ) or ( x = 0 & y = 3 \ 1 ) or ( x = 0 & y = 2 ) or ( x = 0 & y = 3 \ 2 ) or ( x = 0 & y = 3 ) or ( x = 3 \ 1 & y = 0 ) or ( x = 3 \ 1 & y = 3 \ 1 ) or ( x = 3 \ 1 & y = 2 ) or ( x = 1 & y = 0 ) or ( x = 1 & y = 1 ) or ( x = 1 & y = 3 \ 1 ) or ( x = 1 & y = 3 \ 2 ) or ( x = 1 & y = 3 ) or ( x = 1 & y = 2 ) or ( y = 1 & x = 0 ) or ( y = 1 & x = 1 ) or ( y = 1 & x = 3 \ 1 ) or ( y = 1 & x = 3 \ 2 ) or ( y = 1 & x = 3 ) or ( y = 1 & x = 2 ) or ( x = 3 \ 1 & y = 3 \ 2 ) or ( x = 3 \ 1 & y = 3 ) or ( x = 2 & y = 0 ) or ( x = 2 & y = 3 \ 1 ) or ( x = 2 & y = 2 ) or ( x = 2 & y = 3 \ 2 ) or ( x = 2 & y = 3 ) or ( x = 3 \ 2 & y = 0 ) or ( x = 3 \ 2 & y = 3 \ 1 ) or ( x = 3 \ 2 & y = 2 ) or ( x = 3 \ 2 & y = 3 \ 2 ) or ( x = 3 \ 2 & y = 3 ) or ( x = 3 & y = 0 ) or ( x = 3 & y = 3 \ 1 ) or ( x = 3 & y = 2 ) or ( x = 3 & y = 3 \ 2 ) or ( x = 3 & y = 3 ) )
by A3, ENUMSET1:def 4;

end;

suppose
( x = 0 & y = 0 )
; :: thesis: ex z being Element of B_6 st

( x <= z & y <= z & ( for z9 being Element of B_6 st x <= z9 & y <= z9 holds

z <= z9 ) )

( x <= z & y <= z & ( for z9 being Element of B_6 st x <= z9 & y <= z9 holds

z <= z9 ) )

then reconsider z = x \/ y as Element of B_6 ;

take z ; :: thesis: ( x <= z & y <= z & ( for z9 being Element of B_6 st x <= z9 & y <= z9 holds

z <= z9 ) )

( x c= z & y c= z ) by XBOOLE_1:7;

hence ( x <= z & y <= z ) by YELLOW_1:3; :: thesis: for z9 being Element of B_6 st x <= z9 & y <= z9 holds

z <= z9

let w be Element of B_6; :: thesis: ( x <= w & y <= w implies z <= w )

assume ( x <= w & y <= w ) ; :: thesis: z <= w

then ( x c= w & y c= w ) by YELLOW_1:3;

then x \/ y c= w by XBOOLE_1:8;

hence z <= w by YELLOW_1:3; :: thesis: verum

end;take z ; :: thesis: ( x <= z & y <= z & ( for z9 being Element of B_6 st x <= z9 & y <= z9 holds

z <= z9 ) )

( x c= z & y c= z ) by XBOOLE_1:7;

hence ( x <= z & y <= z ) by YELLOW_1:3; :: thesis: for z9 being Element of B_6 st x <= z9 & y <= z9 holds

z <= z9

let w be Element of B_6; :: thesis: ( x <= w & y <= w implies z <= w )

assume ( x <= w & y <= w ) ; :: thesis: z <= w

then ( x c= w & y c= w ) by YELLOW_1:3;

then x \/ y c= w by XBOOLE_1:8;

hence z <= w by YELLOW_1:3; :: thesis: verum

suppose
( x = 0 & y = 3 \ 1 )
; :: thesis: ex z being Element of B_6 st

( x <= z & y <= z & ( for z9 being Element of B_6 st x <= z9 & y <= z9 holds

z <= z9 ) )

( x <= z & y <= z & ( for z9 being Element of B_6 st x <= z9 & y <= z9 holds

z <= z9 ) )

then reconsider z = x \/ y as Element of B_6 ;

take z ; :: thesis: ( x <= z & y <= z & ( for z9 being Element of B_6 st x <= z9 & y <= z9 holds

z <= z9 ) )

( x c= z & y c= z ) by XBOOLE_1:7;

hence ( x <= z & y <= z ) by YELLOW_1:3; :: thesis: for z9 being Element of B_6 st x <= z9 & y <= z9 holds

z <= z9

let w be Element of B_6; :: thesis: ( x <= w & y <= w implies z <= w )

assume ( x <= w & y <= w ) ; :: thesis: z <= w

then ( x c= w & y c= w ) by YELLOW_1:3;

then x \/ y c= w by XBOOLE_1:8;

hence z <= w by YELLOW_1:3; :: thesis: verum

end;take z ; :: thesis: ( x <= z & y <= z & ( for z9 being Element of B_6 st x <= z9 & y <= z9 holds

z <= z9 ) )

( x c= z & y c= z ) by XBOOLE_1:7;

hence ( x <= z & y <= z ) by YELLOW_1:3; :: thesis: for z9 being Element of B_6 st x <= z9 & y <= z9 holds

z <= z9

let w be Element of B_6; :: thesis: ( x <= w & y <= w implies z <= w )

assume ( x <= w & y <= w ) ; :: thesis: z <= w

then ( x c= w & y c= w ) by YELLOW_1:3;

then x \/ y c= w by XBOOLE_1:8;

hence z <= w by YELLOW_1:3; :: thesis: verum

suppose
( x = 0 & y = 2 )
; :: thesis: ex z being Element of B_6 st

( x <= z & y <= z & ( for z9 being Element of B_6 st x <= z9 & y <= z9 holds

z <= z9 ) )

( x <= z & y <= z & ( for z9 being Element of B_6 st x <= z9 & y <= z9 holds

z <= z9 ) )

then reconsider z = x \/ y as Element of B_6 ;

take z ; :: thesis: ( x <= z & y <= z & ( for z9 being Element of B_6 st x <= z9 & y <= z9 holds

z <= z9 ) )

( x c= z & y c= z ) by XBOOLE_1:7;

hence ( x <= z & y <= z ) by YELLOW_1:3; :: thesis: for z9 being Element of B_6 st x <= z9 & y <= z9 holds

z <= z9

let w be Element of B_6; :: thesis: ( x <= w & y <= w implies z <= w )

assume ( x <= w & y <= w ) ; :: thesis: z <= w

then ( x c= w & y c= w ) by YELLOW_1:3;

then x \/ y c= w by XBOOLE_1:8;

hence z <= w by YELLOW_1:3; :: thesis: verum

end;take z ; :: thesis: ( x <= z & y <= z & ( for z9 being Element of B_6 st x <= z9 & y <= z9 holds

z <= z9 ) )

( x c= z & y c= z ) by XBOOLE_1:7;

hence ( x <= z & y <= z ) by YELLOW_1:3; :: thesis: for z9 being Element of B_6 st x <= z9 & y <= z9 holds

z <= z9

let w be Element of B_6; :: thesis: ( x <= w & y <= w implies z <= w )

assume ( x <= w & y <= w ) ; :: thesis: z <= w

then ( x c= w & y c= w ) by YELLOW_1:3;

then x \/ y c= w by XBOOLE_1:8;

hence z <= w by YELLOW_1:3; :: thesis: verum

suppose
( x = 0 & y = 3 \ 2 )
; :: thesis: ex z being Element of B_6 st

( x <= z & y <= z & ( for z9 being Element of B_6 st x <= z9 & y <= z9 holds

z <= z9 ) )

then reconsider z = x \/ y as Element of B_6 ;

take z ; :: thesis: ( x <= z & y <= z & ( for z9 being Element of B_6 st x <= z9 & y <= z9 holds

z <= z9 ) )

( x c= z & y c= z ) by XBOOLE_1:7;

hence ( x <= z & y <= z ) by YELLOW_1:3; :: thesis: for z9 being Element of B_6 st x <= z9 & y <= z9 holds

z <= z9

let w be Element of B_6; :: thesis: ( x <= w & y <= w implies z <= w )

assume ( x <= w & y <= w ) ; :: thesis: z <= w

then ( x c= w & y c= w ) by YELLOW_1:3;

then x \/ y c= w by XBOOLE_1:8;

hence z <= w by YELLOW_1:3; :: thesis: verum

end;

( x <= z & y <= z & ( for z9 being Element of B_6 st x <= z9 & y <= z9 holds

z <= z9 ) )

take z ; :: thesis: ( x <= z & y <= z & ( for z9 being Element of B_6 st x <= z9 & y <= z9 holds

z <= z9 ) )

( x c= z & y c= z ) by XBOOLE_1:7;

hence ( x <= z & y <= z ) by YELLOW_1:3; :: thesis: for z9 being Element of B_6 st x <= z9 & y <= z9 holds

z <= z9

let w be Element of B_6; :: thesis: ( x <= w & y <= w implies z <= w )

assume ( x <= w & y <= w ) ; :: thesis: z <= w

then ( x c= w & y c= w ) by YELLOW_1:3;

then x \/ y c= w by XBOOLE_1:8;

hence z <= w by YELLOW_1:3; :: thesis: verum

suppose
( x = 0 & y = 3 )
; :: thesis: ex z being Element of B_6 st

( x <= z & y <= z & ( for z9 being Element of B_6 st x <= z9 & y <= z9 holds

z <= z9 ) )

then reconsider z = x \/ y as Element of B_6 ;

take z ; :: thesis: ( x <= z & y <= z & ( for z9 being Element of B_6 st x <= z9 & y <= z9 holds

z <= z9 ) )

( x c= z & y c= z ) by XBOOLE_1:7;

hence ( x <= z & y <= z ) by YELLOW_1:3; :: thesis: for z9 being Element of B_6 st x <= z9 & y <= z9 holds

z <= z9

let w be Element of B_6; :: thesis: ( x <= w & y <= w implies z <= w )

assume ( x <= w & y <= w ) ; :: thesis: z <= w

then ( x c= w & y c= w ) by YELLOW_1:3;

then x \/ y c= w by XBOOLE_1:8;

hence z <= w by YELLOW_1:3; :: thesis: verum

end;

( x <= z & y <= z & ( for z9 being Element of B_6 st x <= z9 & y <= z9 holds

z <= z9 ) )

take z ; :: thesis: ( x <= z & y <= z & ( for z9 being Element of B_6 st x <= z9 & y <= z9 holds

z <= z9 ) )

( x c= z & y c= z ) by XBOOLE_1:7;

hence ( x <= z & y <= z ) by YELLOW_1:3; :: thesis: for z9 being Element of B_6 st x <= z9 & y <= z9 holds

z <= z9

let w be Element of B_6; :: thesis: ( x <= w & y <= w implies z <= w )

assume ( x <= w & y <= w ) ; :: thesis: z <= w

then ( x c= w & y c= w ) by YELLOW_1:3;

then x \/ y c= w by XBOOLE_1:8;

hence z <= w by YELLOW_1:3; :: thesis: verum

suppose
( x = 3 \ 1 & y = 0 )
; :: thesis: ex z being Element of B_6 st

( x <= z & y <= z & ( for z9 being Element of B_6 st x <= z9 & y <= z9 holds

z <= z9 ) )

then reconsider z = x \/ y as Element of B_6 ;

take z ; :: thesis: ( x <= z & y <= z & ( for z9 being Element of B_6 st x <= z9 & y <= z9 holds

z <= z9 ) )

( x c= z & y c= z ) by XBOOLE_1:7;

hence ( x <= z & y <= z ) by YELLOW_1:3; :: thesis: for z9 being Element of B_6 st x <= z9 & y <= z9 holds

z <= z9

let w be Element of B_6; :: thesis: ( x <= w & y <= w implies z <= w )

assume ( x <= w & y <= w ) ; :: thesis: z <= w

then ( x c= w & y c= w ) by YELLOW_1:3;

then x \/ y c= w by XBOOLE_1:8;

hence z <= w by YELLOW_1:3; :: thesis: verum

end;

( x <= z & y <= z & ( for z9 being Element of B_6 st x <= z9 & y <= z9 holds

z <= z9 ) )

take z ; :: thesis: ( x <= z & y <= z & ( for z9 being Element of B_6 st x <= z9 & y <= z9 holds

z <= z9 ) )

( x c= z & y c= z ) by XBOOLE_1:7;

hence ( x <= z & y <= z ) by YELLOW_1:3; :: thesis: for z9 being Element of B_6 st x <= z9 & y <= z9 holds

z <= z9

let w be Element of B_6; :: thesis: ( x <= w & y <= w implies z <= w )

assume ( x <= w & y <= w ) ; :: thesis: z <= w

then ( x c= w & y c= w ) by YELLOW_1:3;

then x \/ y c= w by XBOOLE_1:8;

hence z <= w by YELLOW_1:3; :: thesis: verum

suppose
( x = 3 \ 1 & y = 3 \ 1 )
; :: thesis: ex z being Element of B_6 st

( x <= z & y <= z & ( for z9 being Element of B_6 st x <= z9 & y <= z9 holds

z <= z9 ) )

then reconsider z = x \/ y as Element of B_6 ;

take z ; :: thesis: ( x <= z & y <= z & ( for z9 being Element of B_6 st x <= z9 & y <= z9 holds

z <= z9 ) )

( x c= z & y c= z ) by XBOOLE_1:7;

hence ( x <= z & y <= z ) by YELLOW_1:3; :: thesis: for z9 being Element of B_6 st x <= z9 & y <= z9 holds

z <= z9

let w be Element of B_6; :: thesis: ( x <= w & y <= w implies z <= w )

assume ( x <= w & y <= w ) ; :: thesis: z <= w

then ( x c= w & y c= w ) by YELLOW_1:3;

then x \/ y c= w by XBOOLE_1:8;

hence z <= w by YELLOW_1:3; :: thesis: verum

end;

( x <= z & y <= z & ( for z9 being Element of B_6 st x <= z9 & y <= z9 holds

z <= z9 ) )

take z ; :: thesis: ( x <= z & y <= z & ( for z9 being Element of B_6 st x <= z9 & y <= z9 holds

z <= z9 ) )

( x c= z & y c= z ) by XBOOLE_1:7;

hence ( x <= z & y <= z ) by YELLOW_1:3; :: thesis: for z9 being Element of B_6 st x <= z9 & y <= z9 holds

z <= z9

let w be Element of B_6; :: thesis: ( x <= w & y <= w implies z <= w )

assume ( x <= w & y <= w ) ; :: thesis: z <= w

then ( x c= w & y c= w ) by YELLOW_1:3;

then x \/ y c= w by XBOOLE_1:8;

hence z <= w by YELLOW_1:3; :: thesis: verum

suppose A4:
( x = 3 \ 1 & y = 2 )
; :: thesis: ex z being Element of B_6 st

( x <= z & y <= z & ( for z9 being Element of B_6 st x <= z9 & y <= z9 holds

z <= z9 ) )

( x <= z & y <= z & ( for z9 being Element of B_6 st x <= z9 & y <= z9 holds

z <= z9 ) )

3 in {0,1,(3 \ 1),2,(3 \ 2),3}
by ENUMSET1:def 4;

then reconsider z = 3 as Element of B_6 by YELLOW_1:1;

take z ; :: thesis: ( x <= z & y <= z & ( for z9 being Element of B_6 st x <= z9 & y <= z9 holds

z <= z9 ) )

Segm 2 c= Segm 3 by NAT_1:39;

hence ( x <= z & y <= z ) by A4, YELLOW_1:3; :: thesis: for z9 being Element of B_6 st x <= z9 & y <= z9 holds

z <= z9

let z9 be Element of B_6; :: thesis: ( x <= z9 & y <= z9 implies z <= z9 )

assume that

A5: x <= z9 and

A6: y <= z9 ; :: thesis: z <= z9

A7: z9 is Element of {0,1,(3 \ 1),2,(3 \ 2),3} by YELLOW_1:1;

A8: 3 \ 1 c= z9 by A4, A5, YELLOW_1:3;

then ( 1 in z9 & 0 in z9 ) by A11;

then ( z9 <> 1 & z9 <> 0 ) ;

hence z <= z9 by A7, A12, A9, A14, ENUMSET1:def 4; :: thesis: verum

end;then reconsider z = 3 as Element of B_6 by YELLOW_1:1;

take z ; :: thesis: ( x <= z & y <= z & ( for z9 being Element of B_6 st x <= z9 & y <= z9 holds

z <= z9 ) )

Segm 2 c= Segm 3 by NAT_1:39;

hence ( x <= z & y <= z ) by A4, YELLOW_1:3; :: thesis: for z9 being Element of B_6 st x <= z9 & y <= z9 holds

z <= z9

let z9 be Element of B_6; :: thesis: ( x <= z9 & y <= z9 implies z <= z9 )

assume that

A5: x <= z9 and

A6: y <= z9 ; :: thesis: z <= z9

A7: z9 is Element of {0,1,(3 \ 1),2,(3 \ 2),3} by YELLOW_1:1;

A8: 3 \ 1 c= z9 by A4, A5, YELLOW_1:3;

A9: now :: thesis: not z9 = 2

A11:
Segm 2 c= z9
by A4, A6, YELLOW_1:3;assume
z9 = 2
; :: thesis: contradiction

then A10: not 2 in z9 ;

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

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

end;then A10: not 2 in z9 ;

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

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

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

A13:
0 in 2
by CARD_1:50, TARSKI:def 2;

assume z9 = 3 \ 1 ; :: thesis: contradiction

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

end;assume z9 = 3 \ 1 ; :: thesis: contradiction

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

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

( 1 in 2 & 0 in 2 )
by TARSKI:def 2, CARD_1:50;A15:
Segm 1 in Segm 2
by CARD_1:50, TARSKI:def 2;

assume z9 = 3 \ 2 ; :: thesis: contradiction

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

end;assume z9 = 3 \ 2 ; :: thesis: contradiction

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

then ( 1 in z9 & 0 in z9 ) by A11;

then ( z9 <> 1 & z9 <> 0 ) ;

hence z <= z9 by A7, A12, A9, A14, ENUMSET1:def 4; :: thesis: verum

suppose
( x = 1 & y = 0 )
; :: thesis: ex z being Element of B_6 st

( x <= z & y <= z & ( for z9 being Element of B_6 st x <= z9 & y <= z9 holds

z <= z9 ) )

then reconsider z = x \/ y as Element of B_6 ;

take z ; :: thesis: ( x <= z & y <= z & ( for z9 being Element of B_6 st x <= z9 & y <= z9 holds

z <= z9 ) )

( x c= z & y c= z ) by XBOOLE_1:7;

hence ( x <= z & y <= z ) by YELLOW_1:3; :: thesis: for z9 being Element of B_6 st x <= z9 & y <= z9 holds

z <= z9

let w be Element of B_6; :: thesis: ( x <= w & y <= w implies z <= w )

assume ( x <= w & y <= w ) ; :: thesis: z <= w

then ( x c= w & y c= w ) by YELLOW_1:3;

then x \/ y c= w by XBOOLE_1:8;

hence z <= w by YELLOW_1:3; :: thesis: verum

end;

( x <= z & y <= z & ( for z9 being Element of B_6 st x <= z9 & y <= z9 holds

z <= z9 ) )

take z ; :: thesis: ( x <= z & y <= z & ( for z9 being Element of B_6 st x <= z9 & y <= z9 holds

z <= z9 ) )

( x c= z & y c= z ) by XBOOLE_1:7;

hence ( x <= z & y <= z ) by YELLOW_1:3; :: thesis: for z9 being Element of B_6 st x <= z9 & y <= z9 holds

z <= z9

let w be Element of B_6; :: thesis: ( x <= w & y <= w implies z <= w )

assume ( x <= w & y <= w ) ; :: thesis: z <= w

then ( x c= w & y c= w ) by YELLOW_1:3;

then x \/ y c= w by XBOOLE_1:8;

hence z <= w by YELLOW_1:3; :: thesis: verum

suppose
( x = 1 & y = 1 )
; :: thesis: ex z being Element of B_6 st

( x <= z & y <= z & ( for z9 being Element of B_6 st x <= z9 & y <= z9 holds

z <= z9 ) )

then reconsider z = x \/ y as Element of B_6 ;

take z ; :: thesis: ( x <= z & y <= z & ( for z9 being Element of B_6 st x <= z9 & y <= z9 holds

z <= z9 ) )

( x c= z & y c= z ) by XBOOLE_1:7;

hence ( x <= z & y <= z ) by YELLOW_1:3; :: thesis: for z9 being Element of B_6 st x <= z9 & y <= z9 holds

z <= z9

let w be Element of B_6; :: thesis: ( x <= w & y <= w implies z <= w )

assume ( x <= w & y <= w ) ; :: thesis: z <= w

then ( x c= w & y c= w ) by YELLOW_1:3;

then x \/ y c= w by XBOOLE_1:8;

hence z <= w by YELLOW_1:3; :: thesis: verum

end;

( x <= z & y <= z & ( for z9 being Element of B_6 st x <= z9 & y <= z9 holds

z <= z9 ) )

take z ; :: thesis: ( x <= z & y <= z & ( for z9 being Element of B_6 st x <= z9 & y <= z9 holds

z <= z9 ) )

( x c= z & y c= z ) by XBOOLE_1:7;

hence ( x <= z & y <= z ) by YELLOW_1:3; :: thesis: for z9 being Element of B_6 st x <= z9 & y <= z9 holds

z <= z9

let w be Element of B_6; :: thesis: ( x <= w & y <= w implies z <= w )

assume ( x <= w & y <= w ) ; :: thesis: z <= w

then ( x c= w & y c= w ) by YELLOW_1:3;

then x \/ y c= w by XBOOLE_1:8;

hence z <= w by YELLOW_1:3; :: thesis: verum

suppose A16:
( x = 1 & y = 3 \ 1 )
; :: thesis: ex z being Element of B_6 st

( x <= z & y <= z & ( for z9 being Element of B_6 st x <= z9 & y <= z9 holds

z <= z9 ) )

( x <= z & y <= z & ( for z9 being Element of B_6 st x <= z9 & y <= z9 holds

z <= z9 ) )

A17:
Segm 1 c= Segm 3
by NAT_1:39;

1 \/ (3 \ 1) = 1 \/ 3 by XBOOLE_1:39

.= 3 by A17, XBOOLE_1:12 ;

then reconsider z = x \/ y as Element of B_6 by A1, A16, ENUMSET1:def 4;

take z ; :: thesis: ( x <= z & y <= z & ( for z9 being Element of B_6 st x <= z9 & y <= z9 holds

z <= z9 ) )

( x c= z & y c= z ) by XBOOLE_1:7;

hence ( x <= z & y <= z ) by YELLOW_1:3; :: thesis: for z9 being Element of B_6 st x <= z9 & y <= z9 holds

z <= z9

let w be Element of B_6; :: thesis: ( x <= w & y <= w implies z <= w )

assume ( x <= w & y <= w ) ; :: thesis: z <= w

then ( x c= w & y c= w ) by YELLOW_1:3;

then x \/ y c= w by XBOOLE_1:8;

hence z <= w by YELLOW_1:3; :: thesis: verum

end;1 \/ (3 \ 1) = 1 \/ 3 by XBOOLE_1:39

.= 3 by A17, XBOOLE_1:12 ;

then reconsider z = x \/ y as Element of B_6 by A1, A16, ENUMSET1:def 4;

take z ; :: thesis: ( x <= z & y <= z & ( for z9 being Element of B_6 st x <= z9 & y <= z9 holds

z <= z9 ) )

( x c= z & y c= z ) by XBOOLE_1:7;

hence ( x <= z & y <= z ) by YELLOW_1:3; :: thesis: for z9 being Element of B_6 st x <= z9 & y <= z9 holds

z <= z9

let w be Element of B_6; :: thesis: ( x <= w & y <= w implies z <= w )

assume ( x <= w & y <= w ) ; :: thesis: z <= w

then ( x c= w & y c= w ) by YELLOW_1:3;

then x \/ y c= w by XBOOLE_1:8;

hence z <= w by YELLOW_1:3; :: thesis: verum

suppose A18:
( x = 1 & y = 3 \ 2 )
; :: thesis: ex z being Element of B_6 st

( x <= z & y <= z & ( for z9 being Element of B_6 st x <= z9 & y <= z9 holds

z <= z9 ) )

( x <= z & y <= z & ( for z9 being Element of B_6 st x <= z9 & y <= z9 holds

z <= z9 ) )

3 in {0,1,(3 \ 1),2,(3 \ 2),3}
by ENUMSET1:def 4;

then reconsider z = 3 as Element of B_6 by YELLOW_1:1;

take z ; :: thesis: ( x <= z & y <= z & ( for z9 being Element of B_6 st x <= z9 & y <= z9 holds

z <= z9 ) )

Segm 1 c= Segm 3 by NAT_1:39;

hence ( x <= z & y <= z ) by A18, YELLOW_1:3; :: thesis: for z9 being Element of B_6 st x <= z9 & y <= z9 holds

z <= z9

let z9 be Element of B_6; :: thesis: ( x <= z9 & y <= z9 implies z <= z9 )

assume that

A19: x <= z9 and

A20: y <= z9 ; :: thesis: z <= z9

A21: 3 \ 2 c= z9 by A18, A20, YELLOW_1:3;

hence z <= z9 by A27, A24, A29, A22, ENUMSET1:def 4; :: thesis: verum

end;then reconsider z = 3 as Element of B_6 by YELLOW_1:1;

take z ; :: thesis: ( x <= z & y <= z & ( for z9 being Element of B_6 st x <= z9 & y <= z9 holds

z <= z9 ) )

Segm 1 c= Segm 3 by NAT_1:39;

hence ( x <= z & y <= z ) by A18, YELLOW_1:3; :: thesis: for z9 being Element of B_6 st x <= z9 & y <= z9 holds

z <= z9

let z9 be Element of B_6; :: thesis: ( x <= z9 & y <= z9 implies z <= z9 )

assume that

A19: x <= z9 and

A20: y <= z9 ; :: thesis: z <= z9

A21: 3 \ 2 c= z9 by A18, A20, YELLOW_1:3;

A22: now :: thesis: not z9 = 1

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

assume z9 = 1 ; :: thesis: contradiction

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

end;assume z9 = 1 ; :: thesis: contradiction

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

A24: now :: thesis: not z9 = 2

A26:
1 c= z9
by A18, A19, YELLOW_1:3;assume
z9 = 2
; :: thesis: contradiction

then A25: not 2 in z9 ;

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

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

end;then A25: not 2 in z9 ;

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

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

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

A28:
0 in 1
by CARD_1:49, TARSKI:def 1;

assume z9 = 3 \ 1 ; :: thesis: contradiction

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

end;assume z9 = 3 \ 1 ; :: thesis: contradiction

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

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

( z9 is Element of {0,1,(3 \ 1),2,(3 \ 2),3} & z9 <> 0 )
by A26, YELLOW_1:1;A30:
0 in 1
by CARD_1:49, TARSKI:def 1;

assume z9 = 3 \ 2 ; :: thesis: contradiction

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

end;assume z9 = 3 \ 2 ; :: thesis: contradiction

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

hence z <= z9 by A27, A24, A29, A22, ENUMSET1:def 4; :: thesis: verum

suppose A31:
( x = 1 & y = 3 )
; :: thesis: ex z being Element of B_6 st

( x <= z & y <= z & ( for z9 being Element of B_6 st x <= z9 & y <= z9 holds

z <= z9 ) )

( x <= z & y <= z & ( for z9 being Element of B_6 st x <= z9 & y <= z9 holds

z <= z9 ) )

Segm 1 c= Segm 3
by NAT_1:39;

then reconsider z = x \/ y as Element of B_6 by A31, XBOOLE_1:12;

take z ; :: thesis: ( x <= z & y <= z & ( for z9 being Element of B_6 st x <= z9 & y <= z9 holds

z <= z9 ) )

( x c= z & y c= z ) by XBOOLE_1:7;

hence ( x <= z & y <= z ) by YELLOW_1:3; :: thesis: for z9 being Element of B_6 st x <= z9 & y <= z9 holds

z <= z9

let w be Element of B_6; :: thesis: ( x <= w & y <= w implies z <= w )

assume ( x <= w & y <= w ) ; :: thesis: z <= w

then ( x c= w & y c= w ) by YELLOW_1:3;

then x \/ y c= w by XBOOLE_1:8;

hence z <= w by YELLOW_1:3; :: thesis: verum

end;then reconsider z = x \/ y as Element of B_6 by A31, XBOOLE_1:12;

take z ; :: thesis: ( x <= z & y <= z & ( for z9 being Element of B_6 st x <= z9 & y <= z9 holds

z <= z9 ) )

( x c= z & y c= z ) by XBOOLE_1:7;

hence ( x <= z & y <= z ) by YELLOW_1:3; :: thesis: for z9 being Element of B_6 st x <= z9 & y <= z9 holds

z <= z9

let w be Element of B_6; :: thesis: ( x <= w & y <= w implies z <= w )

assume ( x <= w & y <= w ) ; :: thesis: z <= w

then ( x c= w & y c= w ) by YELLOW_1:3;

then x \/ y c= w by XBOOLE_1:8;

hence z <= w by YELLOW_1:3; :: thesis: verum

suppose A32:
( x = 1 & y = 2 )
; :: thesis: ex z being Element of B_6 st

( x <= z & y <= z & ( for z9 being Element of B_6 st x <= z9 & y <= z9 holds

z <= z9 ) )

( x <= z & y <= z & ( for z9 being Element of B_6 st x <= z9 & y <= z9 holds

z <= z9 ) )

Segm 1 c= Segm 2
by NAT_1:39;

then reconsider z = x \/ y as Element of B_6 by A32, XBOOLE_1:12;

take z ; :: thesis: ( x <= z & y <= z & ( for z9 being Element of B_6 st x <= z9 & y <= z9 holds

z <= z9 ) )

( x c= z & y c= z ) by XBOOLE_1:7;

hence ( x <= z & y <= z ) by YELLOW_1:3; :: thesis: for z9 being Element of B_6 st x <= z9 & y <= z9 holds

z <= z9

let w be Element of B_6; :: thesis: ( x <= w & y <= w implies z <= w )

assume ( x <= w & y <= w ) ; :: thesis: z <= w

then ( x c= w & y c= w ) by YELLOW_1:3;

then x \/ y c= w by XBOOLE_1:8;

hence z <= w by YELLOW_1:3; :: thesis: verum

end;then reconsider z = x \/ y as Element of B_6 by A32, XBOOLE_1:12;

take z ; :: thesis: ( x <= z & y <= z & ( for z9 being Element of B_6 st x <= z9 & y <= z9 holds

z <= z9 ) )

( x c= z & y c= z ) by XBOOLE_1:7;

hence ( x <= z & y <= z ) by YELLOW_1:3; :: thesis: for z9 being Element of B_6 st x <= z9 & y <= z9 holds

z <= z9

let w be Element of B_6; :: thesis: ( x <= w & y <= w implies z <= w )

assume ( x <= w & y <= w ) ; :: thesis: z <= w

then ( x c= w & y c= w ) by YELLOW_1:3;

then x \/ y c= w by XBOOLE_1:8;

hence z <= w by YELLOW_1:3; :: thesis: verum

suppose
( y = 1 & x = 0 )
; :: thesis: ex z being Element of B_6 st

( x <= z & y <= z & ( for z9 being Element of B_6 st x <= z9 & y <= z9 holds

z <= z9 ) )

then reconsider z = x \/ y as Element of B_6 ;

take z ; :: thesis: ( x <= z & y <= z & ( for z9 being Element of B_6 st x <= z9 & y <= z9 holds

z <= z9 ) )

( x c= z & y c= z ) by XBOOLE_1:7;

hence ( x <= z & y <= z ) by YELLOW_1:3; :: thesis: for z9 being Element of B_6 st x <= z9 & y <= z9 holds

z <= z9

let w be Element of B_6; :: thesis: ( x <= w & y <= w implies z <= w )

assume ( x <= w & y <= w ) ; :: thesis: z <= w

then ( x c= w & y c= w ) by YELLOW_1:3;

then x \/ y c= w by XBOOLE_1:8;

hence z <= w by YELLOW_1:3; :: thesis: verum

end;

( x <= z & y <= z & ( for z9 being Element of B_6 st x <= z9 & y <= z9 holds

z <= z9 ) )

take z ; :: thesis: ( x <= z & y <= z & ( for z9 being Element of B_6 st x <= z9 & y <= z9 holds

z <= z9 ) )

( x c= z & y c= z ) by XBOOLE_1:7;

hence ( x <= z & y <= z ) by YELLOW_1:3; :: thesis: for z9 being Element of B_6 st x <= z9 & y <= z9 holds

z <= z9

let w be Element of B_6; :: thesis: ( x <= w & y <= w implies z <= w )

assume ( x <= w & y <= w ) ; :: thesis: z <= w

then ( x c= w & y c= w ) by YELLOW_1:3;

then x \/ y c= w by XBOOLE_1:8;

hence z <= w by YELLOW_1:3; :: thesis: verum

suppose
( y = 1 & x = 1 )
; :: thesis: ex z being Element of B_6 st

( x <= z & y <= z & ( for z9 being Element of B_6 st x <= z9 & y <= z9 holds

z <= z9 ) )

then reconsider z = x \/ y as Element of B_6 ;

take z ; :: thesis: ( x <= z & y <= z & ( for z9 being Element of B_6 st x <= z9 & y <= z9 holds

z <= z9 ) )

( x c= z & y c= z ) by XBOOLE_1:7;

hence ( x <= z & y <= z ) by YELLOW_1:3; :: thesis: for z9 being Element of B_6 st x <= z9 & y <= z9 holds

z <= z9

let w be Element of B_6; :: thesis: ( x <= w & y <= w implies z <= w )

assume ( x <= w & y <= w ) ; :: thesis: z <= w

then ( x c= w & y c= w ) by YELLOW_1:3;

then x \/ y c= w by XBOOLE_1:8;

hence z <= w by YELLOW_1:3; :: thesis: verum

end;

( x <= z & y <= z & ( for z9 being Element of B_6 st x <= z9 & y <= z9 holds

z <= z9 ) )

take z ; :: thesis: ( x <= z & y <= z & ( for z9 being Element of B_6 st x <= z9 & y <= z9 holds

z <= z9 ) )

( x c= z & y c= z ) by XBOOLE_1:7;

hence ( x <= z & y <= z ) by YELLOW_1:3; :: thesis: for z9 being Element of B_6 st x <= z9 & y <= z9 holds

z <= z9

let w be Element of B_6; :: thesis: ( x <= w & y <= w implies z <= w )

assume ( x <= w & y <= w ) ; :: thesis: z <= w

then ( x c= w & y c= w ) by YELLOW_1:3;

then x \/ y c= w by XBOOLE_1:8;

hence z <= w by YELLOW_1:3; :: thesis: verum

suppose A33:
( y = 1 & x = 3 \ 1 )
; :: thesis: ex z being Element of B_6 st

( x <= z & y <= z & ( for z9 being Element of B_6 st x <= z9 & y <= z9 holds

z <= z9 ) )

( x <= z & y <= z & ( for z9 being Element of B_6 st x <= z9 & y <= z9 holds

z <= z9 ) )

A34:
Segm 1 c= Segm 3
by NAT_1:39;

1 \/ (3 \ 1) = 1 \/ 3 by XBOOLE_1:39

.= 3 by A34, XBOOLE_1:12 ;

then reconsider z = x \/ y as Element of B_6 by A1, A33, ENUMSET1:def 4;

take z ; :: thesis: ( x <= z & y <= z & ( for z9 being Element of B_6 st x <= z9 & y <= z9 holds

z <= z9 ) )

( x c= z & y c= z ) by XBOOLE_1:7;

hence ( x <= z & y <= z ) by YELLOW_1:3; :: thesis: for z9 being Element of B_6 st x <= z9 & y <= z9 holds

z <= z9

let w be Element of B_6; :: thesis: ( x <= w & y <= w implies z <= w )

assume ( x <= w & y <= w ) ; :: thesis: z <= w

then ( x c= w & y c= w ) by YELLOW_1:3;

then x \/ y c= w by XBOOLE_1:8;

hence z <= w by YELLOW_1:3; :: thesis: verum

end;1 \/ (3 \ 1) = 1 \/ 3 by XBOOLE_1:39

.= 3 by A34, XBOOLE_1:12 ;

then reconsider z = x \/ y as Element of B_6 by A1, A33, ENUMSET1:def 4;

take z ; :: thesis: ( x <= z & y <= z & ( for z9 being Element of B_6 st x <= z9 & y <= z9 holds

z <= z9 ) )

( x c= z & y c= z ) by XBOOLE_1:7;

hence ( x <= z & y <= z ) by YELLOW_1:3; :: thesis: for z9 being Element of B_6 st x <= z9 & y <= z9 holds

z <= z9

let w be Element of B_6; :: thesis: ( x <= w & y <= w implies z <= w )

assume ( x <= w & y <= w ) ; :: thesis: z <= w

then ( x c= w & y c= w ) by YELLOW_1:3;

then x \/ y c= w by XBOOLE_1:8;

hence z <= w by YELLOW_1:3; :: thesis: verum

suppose A35:
( y = 1 & x = 3 \ 2 )
; :: thesis: ex z being Element of B_6 st

( x <= z & y <= z & ( for z9 being Element of B_6 st x <= z9 & y <= z9 holds

z <= z9 ) )

( x <= z & y <= z & ( for z9 being Element of B_6 st x <= z9 & y <= z9 holds

z <= z9 ) )

3 in {0,1,(3 \ 1),2,(3 \ 2),3}
by ENUMSET1:def 4;

then reconsider z = 3 as Element of B_6 by YELLOW_1:1;

take z ; :: thesis: ( x <= z & y <= z & ( for z9 being Element of B_6 st x <= z9 & y <= z9 holds

z <= z9 ) )

Segm 1 c= Segm 3 by NAT_1:39;

hence ( x <= z & y <= z ) by A35, YELLOW_1:3; :: thesis: for z9 being Element of B_6 st x <= z9 & y <= z9 holds

z <= z9

let z9 be Element of B_6; :: thesis: ( x <= z9 & y <= z9 implies z <= z9 )

assume that

A36: x <= z9 and

A37: y <= z9 ; :: thesis: z <= z9

A38: 3 \ 2 c= z9 by A35, A36, YELLOW_1:3;

hence z <= z9 by A44, A41, A46, A39, ENUMSET1:def 4; :: thesis: verum

end;then reconsider z = 3 as Element of B_6 by YELLOW_1:1;

take z ; :: thesis: ( x <= z & y <= z & ( for z9 being Element of B_6 st x <= z9 & y <= z9 holds

z <= z9 ) )

Segm 1 c= Segm 3 by NAT_1:39;

hence ( x <= z & y <= z ) by A35, YELLOW_1:3; :: thesis: for z9 being Element of B_6 st x <= z9 & y <= z9 holds

z <= z9

let z9 be Element of B_6; :: thesis: ( x <= z9 & y <= z9 implies z <= z9 )

assume that

A36: x <= z9 and

A37: y <= z9 ; :: thesis: z <= z9

A38: 3 \ 2 c= z9 by A35, A36, YELLOW_1:3;

A39: now :: thesis: not z9 = 1

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

assume z9 = 1 ; :: thesis: contradiction

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

end;assume z9 = 1 ; :: thesis: contradiction

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

A41: now :: thesis: not z9 = 2

A43:
1 c= z9
by A35, A37, YELLOW_1:3;assume
z9 = 2
; :: thesis: contradiction

then A42: not 2 in z9 ;

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

hence contradiction by A38, A42; :: thesis: verum

end;then A42: not 2 in z9 ;

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

hence contradiction by A38, A42; :: thesis: verum

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

A45:
0 in 1
by CARD_1:49, TARSKI:def 1;

assume z9 = 3 \ 1 ; :: thesis: contradiction

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

end;assume z9 = 3 \ 1 ; :: thesis: contradiction

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

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

( z9 is Element of {0,1,(3 \ 1),2,(3 \ 2),3} & z9 <> 0 )
by A43, YELLOW_1:1;A47:
0 in 1
by CARD_1:49, TARSKI:def 1;

assume z9 = 3 \ 2 ; :: thesis: contradiction

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

end;assume z9 = 3 \ 2 ; :: thesis: contradiction

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

hence z <= z9 by A44, A41, A46, A39, ENUMSET1:def 4; :: thesis: verum

suppose A48:
( y = 1 & x = 3 )
; :: thesis: ex z being Element of B_6 st

( x <= z & y <= z & ( for z9 being Element of B_6 st x <= z9 & y <= z9 holds

z <= z9 ) )

( x <= z & y <= z & ( for z9 being Element of B_6 st x <= z9 & y <= z9 holds

z <= z9 ) )

Segm 1 c= Segm 3
by NAT_1:39;

then reconsider z = x \/ y as Element of B_6 by A48, XBOOLE_1:12;

take z ; :: thesis: ( x <= z & y <= z & ( for z9 being Element of B_6 st x <= z9 & y <= z9 holds

z <= z9 ) )

( x c= z & y c= z ) by XBOOLE_1:7;

hence ( x <= z & y <= z ) by YELLOW_1:3; :: thesis: for z9 being Element of B_6 st x <= z9 & y <= z9 holds

z <= z9

let w be Element of B_6; :: thesis: ( x <= w & y <= w implies z <= w )

assume ( x <= w & y <= w ) ; :: thesis: z <= w

then ( x c= w & y c= w ) by YELLOW_1:3;

then x \/ y c= w by XBOOLE_1:8;

hence z <= w by YELLOW_1:3; :: thesis: verum

end;then reconsider z = x \/ y as Element of B_6 by A48, XBOOLE_1:12;

take z ; :: thesis: ( x <= z & y <= z & ( for z9 being Element of B_6 st x <= z9 & y <= z9 holds

z <= z9 ) )

( x c= z & y c= z ) by XBOOLE_1:7;

hence ( x <= z & y <= z ) by YELLOW_1:3; :: thesis: for z9 being Element of B_6 st x <= z9 & y <= z9 holds

z <= z9

let w be Element of B_6; :: thesis: ( x <= w & y <= w implies z <= w )

assume ( x <= w & y <= w ) ; :: thesis: z <= w

then ( x c= w & y c= w ) by YELLOW_1:3;

then x \/ y c= w by XBOOLE_1:8;

hence z <= w by YELLOW_1:3; :: thesis: verum

suppose A49:
( y = 1 & x = 2 )
; :: thesis: ex z being Element of B_6 st

( x <= z & y <= z & ( for z9 being Element of B_6 st x <= z9 & y <= z9 holds

z <= z9 ) )

( x <= z & y <= z & ( for z9 being Element of B_6 st x <= z9 & y <= z9 holds

z <= z9 ) )

Segm 1 c= Segm 2
by NAT_1:39;

then reconsider z = x \/ y as Element of B_6 by A49, XBOOLE_1:12;

take z ; :: thesis: ( x <= z & y <= z & ( for z9 being Element of B_6 st x <= z9 & y <= z9 holds

z <= z9 ) )

( x c= z & y c= z ) by XBOOLE_1:7;

hence ( x <= z & y <= z ) by YELLOW_1:3; :: thesis: for z9 being Element of B_6 st x <= z9 & y <= z9 holds

z <= z9

let w be Element of B_6; :: thesis: ( x <= w & y <= w implies z <= w )

assume ( x <= w & y <= w ) ; :: thesis: z <= w

then ( x c= w & y c= w ) by YELLOW_1:3;

then x \/ y c= w by XBOOLE_1:8;

hence z <= w by YELLOW_1:3; :: thesis: verum

end;then reconsider z = x \/ y as Element of B_6 by A49, XBOOLE_1:12;

take z ; :: thesis: ( x <= z & y <= z & ( for z9 being Element of B_6 st x <= z9 & y <= z9 holds

z <= z9 ) )

( x c= z & y c= z ) by XBOOLE_1:7;

hence ( x <= z & y <= z ) by YELLOW_1:3; :: thesis: for z9 being Element of B_6 st x <= z9 & y <= z9 holds

z <= z9

let w be Element of B_6; :: thesis: ( x <= w & y <= w implies z <= w )

assume ( x <= w & y <= w ) ; :: thesis: z <= w

then ( x c= w & y c= w ) by YELLOW_1:3;

then x \/ y c= w by XBOOLE_1:8;

hence z <= w by YELLOW_1:3; :: thesis: verum

suppose
( x = 3 \ 1 & y = 3 \ 2 )
; :: thesis: ex z being Element of B_6 st

( x <= z & y <= z & ( for z9 being Element of B_6 st x <= z9 & y <= z9 holds

z <= z9 ) )

( x <= z & y <= z & ( for z9 being Element of B_6 st x <= z9 & y <= z9 holds

z <= z9 ) )

then reconsider z = x \/ y as Element of B_6 by Lm2, XBOOLE_1:12, XBOOLE_1:34;

take z ; :: thesis: ( x <= z & y <= z & ( for z9 being Element of B_6 st x <= z9 & y <= z9 holds

z <= z9 ) )

( x c= z & y c= z ) by XBOOLE_1:7;

hence ( x <= z & y <= z ) by YELLOW_1:3; :: thesis: for z9 being Element of B_6 st x <= z9 & y <= z9 holds

z <= z9

let w be Element of B_6; :: thesis: ( x <= w & y <= w implies z <= w )

assume ( x <= w & y <= w ) ; :: thesis: z <= w

then ( x c= w & y c= w ) by YELLOW_1:3;

then x \/ y c= w by XBOOLE_1:8;

hence z <= w by YELLOW_1:3; :: thesis: verum

end;take z ; :: thesis: ( x <= z & y <= z & ( for z9 being Element of B_6 st x <= z9 & y <= z9 holds

z <= z9 ) )

( x c= z & y c= z ) by XBOOLE_1:7;

hence ( x <= z & y <= z ) by YELLOW_1:3; :: thesis: for z9 being Element of B_6 st x <= z9 & y <= z9 holds

z <= z9

let w be Element of B_6; :: thesis: ( x <= w & y <= w implies z <= w )

assume ( x <= w & y <= w ) ; :: thesis: z <= w

then ( x c= w & y c= w ) by YELLOW_1:3;

then x \/ y c= w by XBOOLE_1:8;

hence z <= w by YELLOW_1:3; :: thesis: verum

suppose
( x = 3 \ 1 & y = 3 )
; :: thesis: ex z being Element of B_6 st

( x <= z & y <= z & ( for z9 being Element of B_6 st x <= z9 & y <= z9 holds

z <= z9 ) )

( x <= z & y <= z & ( for z9 being Element of B_6 st x <= z9 & y <= z9 holds

z <= z9 ) )

then reconsider z = x \/ y as Element of B_6 by XBOOLE_1:12;

take z ; :: thesis: ( x <= z & y <= z & ( for z9 being Element of B_6 st x <= z9 & y <= z9 holds

z <= z9 ) )

( x c= z & y c= z ) by XBOOLE_1:7;

hence ( x <= z & y <= z ) by YELLOW_1:3; :: thesis: for z9 being Element of B_6 st x <= z9 & y <= z9 holds

z <= z9

let w be Element of B_6; :: thesis: ( x <= w & y <= w implies z <= w )

assume ( x <= w & y <= w ) ; :: thesis: z <= w

then ( x c= w & y c= w ) by YELLOW_1:3;

then x \/ y c= w by XBOOLE_1:8;

hence z <= w by YELLOW_1:3; :: thesis: verum

end;take z ; :: thesis: ( x <= z & y <= z & ( for z9 being Element of B_6 st x <= z9 & y <= z9 holds

z <= z9 ) )

( x c= z & y c= z ) by XBOOLE_1:7;

hence ( x <= z & y <= z ) by YELLOW_1:3; :: thesis: for z9 being Element of B_6 st x <= z9 & y <= z9 holds

z <= z9

let w be Element of B_6; :: thesis: ( x <= w & y <= w implies z <= w )

assume ( x <= w & y <= w ) ; :: thesis: z <= w

then ( x c= w & y c= w ) by YELLOW_1:3;

then x \/ y c= w by XBOOLE_1:8;

hence z <= w by YELLOW_1:3; :: thesis: verum

suppose
( x = 2 & y = 0 )
; :: thesis: ex z being Element of B_6 st

( x <= z & y <= z & ( for z9 being Element of B_6 st x <= z9 & y <= z9 holds

z <= z9 ) )

then reconsider z = x \/ y as Element of B_6 ;

take z ; :: thesis: ( x <= z & y <= z & ( for z9 being Element of B_6 st x <= z9 & y <= z9 holds

z <= z9 ) )

( x c= z & y c= z ) by XBOOLE_1:7;

hence ( x <= z & y <= z ) by YELLOW_1:3; :: thesis: for z9 being Element of B_6 st x <= z9 & y <= z9 holds

z <= z9

let w be Element of B_6; :: thesis: ( x <= w & y <= w implies z <= w )

assume ( x <= w & y <= w ) ; :: thesis: z <= w

then ( x c= w & y c= w ) by YELLOW_1:3;

then x \/ y c= w by XBOOLE_1:8;

hence z <= w by YELLOW_1:3; :: thesis: verum

end;

( x <= z & y <= z & ( for z9 being Element of B_6 st x <= z9 & y <= z9 holds

z <= z9 ) )

take z ; :: thesis: ( x <= z & y <= z & ( for z9 being Element of B_6 st x <= z9 & y <= z9 holds

z <= z9 ) )

( x c= z & y c= z ) by XBOOLE_1:7;

hence ( x <= z & y <= z ) by YELLOW_1:3; :: thesis: for z9 being Element of B_6 st x <= z9 & y <= z9 holds

z <= z9

let w be Element of B_6; :: thesis: ( x <= w & y <= w implies z <= w )

assume ( x <= w & y <= w ) ; :: thesis: z <= w

then ( x c= w & y c= w ) by YELLOW_1:3;

then x \/ y c= w by XBOOLE_1:8;

hence z <= w by YELLOW_1:3; :: thesis: verum

suppose A50:
( x = 2 & y = 3 \ 1 )
; :: thesis: ex z being Element of B_6 st

( x <= z & y <= z & ( for z9 being Element of B_6 st x <= z9 & y <= z9 holds

z <= z9 ) )

( x <= z & y <= z & ( for z9 being Element of B_6 st x <= z9 & y <= z9 holds

z <= z9 ) )

3 in {0,1,(3 \ 1),2,(3 \ 2),3}
by ENUMSET1:def 4;

then reconsider z = 3 as Element of B_6 by YELLOW_1:1;

take z ; :: thesis: ( x <= z & y <= z & ( for z9 being Element of B_6 st x <= z9 & y <= z9 holds

z <= z9 ) )

Segm 2 c= Segm 3 by NAT_1:39;

hence ( x <= z & y <= z ) by A50, YELLOW_1:3; :: thesis: for z9 being Element of B_6 st x <= z9 & y <= z9 holds

z <= z9

let z9 be Element of B_6; :: thesis: ( x <= z9 & y <= z9 implies z <= z9 )

assume that

A51: x <= z9 and

A52: y <= z9 ; :: thesis: z <= z9

A53: z9 is Element of {0,1,(3 \ 1),2,(3 \ 2),3} by YELLOW_1:1;

A54: 3 \ 1 c= z9 by A50, A52, YELLOW_1:3;

then ( 1 in z9 & 0 in z9 ) by A57;

then ( z9 <> 1 & z9 <> 0 ) ;

hence z <= z9 by A53, A58, A55, A60, ENUMSET1:def 4; :: thesis: verum

end;then reconsider z = 3 as Element of B_6 by YELLOW_1:1;

take z ; :: thesis: ( x <= z & y <= z & ( for z9 being Element of B_6 st x <= z9 & y <= z9 holds

z <= z9 ) )

Segm 2 c= Segm 3 by NAT_1:39;

hence ( x <= z & y <= z ) by A50, YELLOW_1:3; :: thesis: for z9 being Element of B_6 st x <= z9 & y <= z9 holds

z <= z9

let z9 be Element of B_6; :: thesis: ( x <= z9 & y <= z9 implies z <= z9 )

assume that

A51: x <= z9 and

A52: y <= z9 ; :: thesis: z <= z9

A53: z9 is Element of {0,1,(3 \ 1),2,(3 \ 2),3} by YELLOW_1:1;

A54: 3 \ 1 c= z9 by A50, A52, YELLOW_1:3;

A55: now :: thesis: not z9 = 2

A57:
2 c= z9
by A50, A51, YELLOW_1:3;assume
z9 = 2
; :: thesis: contradiction

then A56: not 2 in z9 ;

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

hence contradiction by A54, A56; :: thesis: verum

end;then A56: not 2 in z9 ;

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

hence contradiction by A54, A56; :: thesis: verum

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

A59:
0 in 2
by CARD_1:50, TARSKI:def 2;

assume z9 = 3 \ 1 ; :: thesis: contradiction

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

end;assume z9 = 3 \ 1 ; :: thesis: contradiction

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

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

( 1 in 2 & 0 in 2 )
by CARD_1:50, TARSKI:def 2;A61:
1 in 2
by CARD_1:50, TARSKI:def 2;

assume z9 = 3 \ 2 ; :: thesis: contradiction

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

end;assume z9 = 3 \ 2 ; :: thesis: contradiction

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

then ( 1 in z9 & 0 in z9 ) by A57;

then ( z9 <> 1 & z9 <> 0 ) ;

hence z <= z9 by A53, A58, A55, A60, ENUMSET1:def 4; :: thesis: verum

suppose
( x = 2 & y = 2 )
; :: thesis: ex z being Element of B_6 st

( x <= z & y <= z & ( for z9 being Element of B_6 st x <= z9 & y <= z9 holds

z <= z9 ) )

then reconsider z = x \/ y as Element of B_6 ;

take z ; :: thesis: ( x <= z & y <= z & ( for z9 being Element of B_6 st x <= z9 & y <= z9 holds

z <= z9 ) )

( x c= z & y c= z ) by XBOOLE_1:7;

hence ( x <= z & y <= z ) by YELLOW_1:3; :: thesis: for z9 being Element of B_6 st x <= z9 & y <= z9 holds

z <= z9

let w be Element of B_6; :: thesis: ( x <= w & y <= w implies z <= w )

assume ( x <= w & y <= w ) ; :: thesis: z <= w

then ( x c= w & y c= w ) by YELLOW_1:3;

then x \/ y c= w by XBOOLE_1:8;

hence z <= w by YELLOW_1:3; :: thesis: verum

end;

( x <= z & y <= z & ( for z9 being Element of B_6 st x <= z9 & y <= z9 holds

z <= z9 ) )

take z ; :: thesis: ( x <= z & y <= z & ( for z9 being Element of B_6 st x <= z9 & y <= z9 holds

z <= z9 ) )

( x c= z & y c= z ) by XBOOLE_1:7;

hence ( x <= z & y <= z ) by YELLOW_1:3; :: thesis: for z9 being Element of B_6 st x <= z9 & y <= z9 holds

z <= z9

let w be Element of B_6; :: thesis: ( x <= w & y <= w implies z <= w )

assume ( x <= w & y <= w ) ; :: thesis: z <= w

then ( x c= w & y c= w ) by YELLOW_1:3;

then x \/ y c= w by XBOOLE_1:8;

hence z <= w by YELLOW_1:3; :: thesis: verum

suppose A62:
( x = 2 & y = 3 \ 2 )
; :: thesis: ex z being Element of B_6 st

( x <= z & y <= z & ( for z9 being Element of B_6 st x <= z9 & y <= z9 holds

z <= z9 ) )

( x <= z & y <= z & ( for z9 being Element of B_6 st x <= z9 & y <= z9 holds

z <= z9 ) )

A63:
Segm 2 c= Segm 3
by NAT_1:39;

2 \/ (3 \ 2) = 2 \/ 3 by XBOOLE_1:39

.= 3 by A63, XBOOLE_1:12 ;

then x \/ y in {0,1,(3 \ 1),2,(3 \ 2),3} by A62, ENUMSET1:def 4;

then reconsider z = x \/ y as Element of B_6 by YELLOW_1:1;

take z ; :: thesis: ( x <= z & y <= z & ( for z9 being Element of B_6 st x <= z9 & y <= z9 holds

z <= z9 ) )

( x c= z & y c= z ) by XBOOLE_1:7;

hence ( x <= z & y <= z ) by YELLOW_1:3; :: thesis: for z9 being Element of B_6 st x <= z9 & y <= z9 holds

z <= z9

let w be Element of B_6; :: thesis: ( x <= w & y <= w implies z <= w )

assume ( x <= w & y <= w ) ; :: thesis: z <= w

then ( x c= w & y c= w ) by YELLOW_1:3;

then x \/ y c= w by XBOOLE_1:8;

hence z <= w by YELLOW_1:3; :: thesis: verum

end;2 \/ (3 \ 2) = 2 \/ 3 by XBOOLE_1:39

.= 3 by A63, XBOOLE_1:12 ;

then x \/ y in {0,1,(3 \ 1),2,(3 \ 2),3} by A62, ENUMSET1:def 4;

then reconsider z = x \/ y as Element of B_6 by YELLOW_1:1;

take z ; :: thesis: ( x <= z & y <= z & ( for z9 being Element of B_6 st x <= z9 & y <= z9 holds

z <= z9 ) )

( x c= z & y c= z ) by XBOOLE_1:7;

hence ( x <= z & y <= z ) by YELLOW_1:3; :: thesis: for z9 being Element of B_6 st x <= z9 & y <= z9 holds

z <= z9

let w be Element of B_6; :: thesis: ( x <= w & y <= w implies z <= w )

assume ( x <= w & y <= w ) ; :: thesis: z <= w

then ( x c= w & y c= w ) by YELLOW_1:3;

then x \/ y c= w by XBOOLE_1:8;

hence z <= w by YELLOW_1:3; :: thesis: verum

suppose A64:
( x = 2 & y = 3 )
; :: thesis: ex z being Element of B_6 st

( x <= z & y <= z & ( for z9 being Element of B_6 st x <= z9 & y <= z9 holds

z <= z9 ) )

( x <= z & y <= z & ( for z9 being Element of B_6 st x <= z9 & y <= z9 holds

z <= z9 ) )

Segm 2 c= Segm 3
by NAT_1:39;

then reconsider z = x \/ y as Element of B_6 by A64, XBOOLE_1:12;

take z ; :: thesis: ( x <= z & y <= z & ( for z9 being Element of B_6 st x <= z9 & y <= z9 holds

z <= z9 ) )

( x c= z & y c= z ) by XBOOLE_1:7;

hence ( x <= z & y <= z ) by YELLOW_1:3; :: thesis: for z9 being Element of B_6 st x <= z9 & y <= z9 holds

z <= z9

let w be Element of B_6; :: thesis: ( x <= w & y <= w implies z <= w )

assume ( x <= w & y <= w ) ; :: thesis: z <= w

then ( x c= w & y c= w ) by YELLOW_1:3;

then x \/ y c= w by XBOOLE_1:8;

hence z <= w by YELLOW_1:3; :: thesis: verum

end;then reconsider z = x \/ y as Element of B_6 by A64, XBOOLE_1:12;

take z ; :: thesis: ( x <= z & y <= z & ( for z9 being Element of B_6 st x <= z9 & y <= z9 holds

z <= z9 ) )

( x c= z & y c= z ) by XBOOLE_1:7;

hence ( x <= z & y <= z ) by YELLOW_1:3; :: thesis: for z9 being Element of B_6 st x <= z9 & y <= z9 holds

z <= z9

let w be Element of B_6; :: thesis: ( x <= w & y <= w implies z <= w )

assume ( x <= w & y <= w ) ; :: thesis: z <= w

then ( x c= w & y c= w ) by YELLOW_1:3;

then x \/ y c= w by XBOOLE_1:8;

hence z <= w by YELLOW_1:3; :: thesis: verum

suppose
( x = 3 \ 2 & y = 0 )
; :: thesis: ex z being Element of B_6 st

( x <= z & y <= z & ( for z9 being Element of B_6 st x <= z9 & y <= z9 holds

z <= z9 ) )

then reconsider z = x \/ y as Element of B_6 ;

take z ; :: thesis: ( x <= z & y <= z & ( for z9 being Element of B_6 st x <= z9 & y <= z9 holds

z <= z9 ) )

( x c= z & y c= z ) by XBOOLE_1:7;

hence ( x <= z & y <= z ) by YELLOW_1:3; :: thesis: for z9 being Element of B_6 st x <= z9 & y <= z9 holds

z <= z9

let w be Element of B_6; :: thesis: ( x <= w & y <= w implies z <= w )

assume ( x <= w & y <= w ) ; :: thesis: z <= w

then ( x c= w & y c= w ) by YELLOW_1:3;

then x \/ y c= w by XBOOLE_1:8;

hence z <= w by YELLOW_1:3; :: thesis: verum

end;

( x <= z & y <= z & ( for z9 being Element of B_6 st x <= z9 & y <= z9 holds

z <= z9 ) )

take z ; :: thesis: ( x <= z & y <= z & ( for z9 being Element of B_6 st x <= z9 & y <= z9 holds

z <= z9 ) )

( x c= z & y c= z ) by XBOOLE_1:7;

hence ( x <= z & y <= z ) by YELLOW_1:3; :: thesis: for z9 being Element of B_6 st x <= z9 & y <= z9 holds

z <= z9

let w be Element of B_6; :: thesis: ( x <= w & y <= w implies z <= w )

assume ( x <= w & y <= w ) ; :: thesis: z <= w

then ( x c= w & y c= w ) by YELLOW_1:3;

then x \/ y c= w by XBOOLE_1:8;

hence z <= w by YELLOW_1:3; :: thesis: verum

suppose
( x = 3 \ 2 & y = 3 \ 1 )
; :: thesis: ex z being Element of B_6 st

( x <= z & y <= z & ( for z9 being Element of B_6 st x <= z9 & y <= z9 holds

z <= z9 ) )

( x <= z & y <= z & ( for z9 being Element of B_6 st x <= z9 & y <= z9 holds

z <= z9 ) )

then reconsider z = x \/ y as Element of B_6 by Lm2, XBOOLE_1:12, XBOOLE_1:34;

take z ; :: thesis: ( x <= z & y <= z & ( for z9 being Element of B_6 st x <= z9 & y <= z9 holds

z <= z9 ) )

( x c= z & y c= z ) by XBOOLE_1:7;

hence ( x <= z & y <= z ) by YELLOW_1:3; :: thesis: for z9 being Element of B_6 st x <= z9 & y <= z9 holds

z <= z9

let w be Element of B_6; :: thesis: ( x <= w & y <= w implies z <= w )

assume ( x <= w & y <= w ) ; :: thesis: z <= w

then ( x c= w & y c= w ) by YELLOW_1:3;

then x \/ y c= w by XBOOLE_1:8;

hence z <= w by YELLOW_1:3; :: thesis: verum

end;take z ; :: thesis: ( x <= z & y <= z & ( for z9 being Element of B_6 st x <= z9 & y <= z9 holds

z <= z9 ) )

( x c= z & y c= z ) by XBOOLE_1:7;

hence ( x <= z & y <= z ) by YELLOW_1:3; :: thesis: for z9 being Element of B_6 st x <= z9 & y <= z9 holds

z <= z9

let w be Element of B_6; :: thesis: ( x <= w & y <= w implies z <= w )

assume ( x <= w & y <= w ) ; :: thesis: z <= w

then ( x c= w & y c= w ) by YELLOW_1:3;

then x \/ y c= w by XBOOLE_1:8;

hence z <= w by YELLOW_1:3; :: thesis: verum

suppose A65:
( x = 3 \ 2 & y = 2 )
; :: thesis: ex z being Element of B_6 st

( x <= z & y <= z & ( for z9 being Element of B_6 st x <= z9 & y <= z9 holds

z <= z9 ) )

( x <= z & y <= z & ( for z9 being Element of B_6 st x <= z9 & y <= z9 holds

z <= z9 ) )

A66:
Segm 2 c= Segm 3
by NAT_1:39;

2 \/ (3 \ 2) = 2 \/ 3 by XBOOLE_1:39

.= 3 by A66, XBOOLE_1:12 ;

then x \/ y in {0,1,(3 \ 1),2,(3 \ 2),3} by A65, ENUMSET1:def 4;

then reconsider z = x \/ y as Element of B_6 by YELLOW_1:1;

take z ; :: thesis: ( x <= z & y <= z & ( for z9 being Element of B_6 st x <= z9 & y <= z9 holds

z <= z9 ) )

( x c= z & y c= z ) by XBOOLE_1:7;

hence ( x <= z & y <= z ) by YELLOW_1:3; :: thesis: for z9 being Element of B_6 st x <= z9 & y <= z9 holds

z <= z9

let w be Element of B_6; :: thesis: ( x <= w & y <= w implies z <= w )

assume ( x <= w & y <= w ) ; :: thesis: z <= w

then ( x c= w & y c= w ) by YELLOW_1:3;

then x \/ y c= w by XBOOLE_1:8;

hence z <= w by YELLOW_1:3; :: thesis: verum

end;2 \/ (3 \ 2) = 2 \/ 3 by XBOOLE_1:39

.= 3 by A66, XBOOLE_1:12 ;

then x \/ y in {0,1,(3 \ 1),2,(3 \ 2),3} by A65, ENUMSET1:def 4;

then reconsider z = x \/ y as Element of B_6 by YELLOW_1:1;

take z ; :: thesis: ( x <= z & y <= z & ( for z9 being Element of B_6 st x <= z9 & y <= z9 holds

z <= z9 ) )

( x c= z & y c= z ) by XBOOLE_1:7;

hence ( x <= z & y <= z ) by YELLOW_1:3; :: thesis: for z9 being Element of B_6 st x <= z9 & y <= z9 holds

z <= z9

let w be Element of B_6; :: thesis: ( x <= w & y <= w implies z <= w )

assume ( x <= w & y <= w ) ; :: thesis: z <= w

then ( x c= w & y c= w ) by YELLOW_1:3;

then x \/ y c= w by XBOOLE_1:8;

hence z <= w by YELLOW_1:3; :: thesis: verum

suppose
( x = 3 \ 2 & y = 3 \ 2 )
; :: thesis: ex z being Element of B_6 st

( x <= z & y <= z & ( for z9 being Element of B_6 st x <= z9 & y <= z9 holds

z <= z9 ) )

then reconsider z = x \/ y as Element of B_6 ;

take z ; :: thesis: ( x <= z & y <= z & ( for z9 being Element of B_6 st x <= z9 & y <= z9 holds

z <= z9 ) )

( x c= z & y c= z ) by XBOOLE_1:7;

hence ( x <= z & y <= z ) by YELLOW_1:3; :: thesis: for z9 being Element of B_6 st x <= z9 & y <= z9 holds

z <= z9

let w be Element of B_6; :: thesis: ( x <= w & y <= w implies z <= w )

assume ( x <= w & y <= w ) ; :: thesis: z <= w

then ( x c= w & y c= w ) by YELLOW_1:3;

then x \/ y c= w by XBOOLE_1:8;

hence z <= w by YELLOW_1:3; :: thesis: verum

end;

( x <= z & y <= z & ( for z9 being Element of B_6 st x <= z9 & y <= z9 holds

z <= z9 ) )

take z ; :: thesis: ( x <= z & y <= z & ( for z9 being Element of B_6 st x <= z9 & y <= z9 holds

z <= z9 ) )

( x c= z & y c= z ) by XBOOLE_1:7;

hence ( x <= z & y <= z ) by YELLOW_1:3; :: thesis: for z9 being Element of B_6 st x <= z9 & y <= z9 holds

z <= z9

let w be Element of B_6; :: thesis: ( x <= w & y <= w implies z <= w )

assume ( x <= w & y <= w ) ; :: thesis: z <= w

then ( x c= w & y c= w ) by YELLOW_1:3;

then x \/ y c= w by XBOOLE_1:8;

hence z <= w by YELLOW_1:3; :: thesis: verum

suppose
( x = 3 \ 2 & y = 3 )
; :: thesis: ex z being Element of B_6 st

( x <= z & y <= z & ( for z9 being Element of B_6 st x <= z9 & y <= z9 holds

z <= z9 ) )

( x <= z & y <= z & ( for z9 being Element of B_6 st x <= z9 & y <= z9 holds

z <= z9 ) )

then reconsider z = x \/ y as Element of B_6 by XBOOLE_1:12;

take z ; :: thesis: ( x <= z & y <= z & ( for z9 being Element of B_6 st x <= z9 & y <= z9 holds

z <= z9 ) )

( x c= z & y c= z ) by XBOOLE_1:7;

hence ( x <= z & y <= z ) by YELLOW_1:3; :: thesis: for z9 being Element of B_6 st x <= z9 & y <= z9 holds

z <= z9

let w be Element of B_6; :: thesis: ( x <= w & y <= w implies z <= w )

assume ( x <= w & y <= w ) ; :: thesis: z <= w

then ( x c= w & y c= w ) by YELLOW_1:3;

then x \/ y c= w by XBOOLE_1:8;

hence z <= w by YELLOW_1:3; :: thesis: verum

end;take z ; :: thesis: ( x <= z & y <= z & ( for z9 being Element of B_6 st x <= z9 & y <= z9 holds

z <= z9 ) )

( x c= z & y c= z ) by XBOOLE_1:7;

hence ( x <= z & y <= z ) by YELLOW_1:3; :: thesis: for z9 being Element of B_6 st x <= z9 & y <= z9 holds

z <= z9

let w be Element of B_6; :: thesis: ( x <= w & y <= w implies z <= w )

assume ( x <= w & y <= w ) ; :: thesis: z <= w

then ( x c= w & y c= w ) by YELLOW_1:3;

then x \/ y c= w by XBOOLE_1:8;

hence z <= w by YELLOW_1:3; :: thesis: verum

suppose
( x = 3 & y = 0 )
; :: thesis: ex z being Element of B_6 st

( x <= z & y <= z & ( for z9 being Element of B_6 st x <= z9 & y <= z9 holds

z <= z9 ) )

then reconsider z = x \/ y as Element of B_6 ;

take z ; :: thesis: ( x <= z & y <= z & ( for z9 being Element of B_6 st x <= z9 & y <= z9 holds

z <= z9 ) )

( x c= z & y c= z ) by XBOOLE_1:7;

hence ( x <= z & y <= z ) by YELLOW_1:3; :: thesis: for z9 being Element of B_6 st x <= z9 & y <= z9 holds

z <= z9

let w be Element of B_6; :: thesis: ( x <= w & y <= w implies z <= w )

assume ( x <= w & y <= w ) ; :: thesis: z <= w

then ( x c= w & y c= w ) by YELLOW_1:3;

then x \/ y c= w by XBOOLE_1:8;

hence z <= w by YELLOW_1:3; :: thesis: verum

end;

( x <= z & y <= z & ( for z9 being Element of B_6 st x <= z9 & y <= z9 holds

z <= z9 ) )

take z ; :: thesis: ( x <= z & y <= z & ( for z9 being Element of B_6 st x <= z9 & y <= z9 holds

z <= z9 ) )

( x c= z & y c= z ) by XBOOLE_1:7;

hence ( x <= z & y <= z ) by YELLOW_1:3; :: thesis: for z9 being Element of B_6 st x <= z9 & y <= z9 holds

z <= z9

let w be Element of B_6; :: thesis: ( x <= w & y <= w implies z <= w )

assume ( x <= w & y <= w ) ; :: thesis: z <= w

then ( x c= w & y c= w ) by YELLOW_1:3;

then x \/ y c= w by XBOOLE_1:8;

hence z <= w by YELLOW_1:3; :: thesis: verum

suppose
( x = 3 & y = 3 \ 1 )
; :: thesis: ex z being Element of B_6 st

( x <= z & y <= z & ( for z9 being Element of B_6 st x <= z9 & y <= z9 holds

z <= z9 ) )

( x <= z & y <= z & ( for z9 being Element of B_6 st x <= z9 & y <= z9 holds

z <= z9 ) )

then reconsider z = x \/ y as Element of B_6 by XBOOLE_1:12;

take z ; :: thesis: ( x <= z & y <= z & ( for z9 being Element of B_6 st x <= z9 & y <= z9 holds

z <= z9 ) )

( x c= z & y c= z ) by XBOOLE_1:7;

hence ( x <= z & y <= z ) by YELLOW_1:3; :: thesis: for z9 being Element of B_6 st x <= z9 & y <= z9 holds

z <= z9

let w be Element of B_6; :: thesis: ( x <= w & y <= w implies z <= w )

assume ( x <= w & y <= w ) ; :: thesis: z <= w

then ( x c= w & y c= w ) by YELLOW_1:3;

then x \/ y c= w by XBOOLE_1:8;

hence z <= w by YELLOW_1:3; :: thesis: verum

end;take z ; :: thesis: ( x <= z & y <= z & ( for z9 being Element of B_6 st x <= z9 & y <= z9 holds

z <= z9 ) )

( x c= z & y c= z ) by XBOOLE_1:7;

hence ( x <= z & y <= z ) by YELLOW_1:3; :: thesis: for z9 being Element of B_6 st x <= z9 & y <= z9 holds

z <= z9

let w be Element of B_6; :: thesis: ( x <= w & y <= w implies z <= w )

assume ( x <= w & y <= w ) ; :: thesis: z <= w

then ( x c= w & y c= w ) by YELLOW_1:3;

then x \/ y c= w by XBOOLE_1:8;

hence z <= w by YELLOW_1:3; :: thesis: verum

suppose A67:
( x = 3 & y = 2 )
; :: thesis: ex z being Element of B_6 st

( x <= z & y <= z & ( for z9 being Element of B_6 st x <= z9 & y <= z9 holds

z <= z9 ) )

( x <= z & y <= z & ( for z9 being Element of B_6 st x <= z9 & y <= z9 holds

z <= z9 ) )

Segm 2 c= Segm 3
by NAT_1:39;

then reconsider z = x \/ y as Element of B_6 by A67, XBOOLE_1:12;

take z ; :: thesis: ( x <= z & y <= z & ( for z9 being Element of B_6 st x <= z9 & y <= z9 holds

z <= z9 ) )

( x c= z & y c= z ) by XBOOLE_1:7;

hence ( x <= z & y <= z ) by YELLOW_1:3; :: thesis: for z9 being Element of B_6 st x <= z9 & y <= z9 holds

z <= z9

let w be Element of B_6; :: thesis: ( x <= w & y <= w implies z <= w )

assume ( x <= w & y <= w ) ; :: thesis: z <= w

then ( x c= w & y c= w ) by YELLOW_1:3;

then x \/ y c= w by XBOOLE_1:8;

hence z <= w by YELLOW_1:3; :: thesis: verum

end;then reconsider z = x \/ y as Element of B_6 by A67, XBOOLE_1:12;

take z ; :: thesis: ( x <= z & y <= z & ( for z9 being Element of B_6 st x <= z9 & y <= z9 holds

z <= z9 ) )

( x c= z & y c= z ) by XBOOLE_1:7;

hence ( x <= z & y <= z ) by YELLOW_1:3; :: thesis: for z9 being Element of B_6 st x <= z9 & y <= z9 holds

z <= z9

let w be Element of B_6; :: thesis: ( x <= w & y <= w implies z <= w )

assume ( x <= w & y <= w ) ; :: thesis: z <= w

then ( x c= w & y c= w ) by YELLOW_1:3;

then x \/ y c= w by XBOOLE_1:8;

hence z <= w by YELLOW_1:3; :: thesis: verum

suppose
( x = 3 & y = 3 \ 2 )
; :: thesis: ex z being Element of B_6 st

( x <= z & y <= z & ( for z9 being Element of B_6 st x <= z9 & y <= z9 holds

z <= z9 ) )

then reconsider z = x \/ y as Element of B_6 by XBOOLE_1:12;

take z ; :: thesis: ( x <= z & y <= z & ( for z9 being Element of B_6 st x <= z9 & y <= z9 holds

z <= z9 ) )

( x c= z & y c= z ) by XBOOLE_1:7;

hence ( x <= z & y <= z ) by YELLOW_1:3; :: thesis: for z9 being Element of B_6 st x <= z9 & y <= z9 holds

z <= z9

let w be Element of B_6; :: thesis: ( x <= w & y <= w implies z <= w )

assume ( x <= w & y <= w ) ; :: thesis: z <= w

then ( x c= w & y c= w ) by YELLOW_1:3;

then x \/ y c= w by XBOOLE_1:8;

hence z <= w by YELLOW_1:3; :: thesis: verum

end;

( x <= z & y <= z & ( for z9 being Element of B_6 st x <= z9 & y <= z9 holds

z <= z9 ) )

take z ; :: thesis: ( x <= z & y <= z & ( for z9 being Element of B_6 st x <= z9 & y <= z9 holds

z <= z9 ) )

( x c= z & y c= z ) by XBOOLE_1:7;

hence ( x <= z & y <= z ) by YELLOW_1:3; :: thesis: for z9 being Element of B_6 st x <= z9 & y <= z9 holds

z <= z9

let w be Element of B_6; :: thesis: ( x <= w & y <= w implies z <= w )

assume ( x <= w & y <= w ) ; :: thesis: z <= w

then ( x c= w & y c= w ) by YELLOW_1:3;

then x \/ y c= w by XBOOLE_1:8;

hence z <= w by YELLOW_1:3; :: thesis: verum

suppose
( x = 3 & y = 3 )
; :: thesis: ex z being Element of B_6 st

( x <= z & y <= z & ( for z9 being Element of B_6 st x <= z9 & y <= z9 holds

z <= z9 ) )

then reconsider z = x \/ y as Element of B_6 ;

take z ; :: thesis: ( x <= z & y <= z & ( for z9 being Element of B_6 st x <= z9 & y <= z9 holds

z <= z9 ) )

( x c= z & y c= z ) by XBOOLE_1:7;

hence ( x <= z & y <= z ) by YELLOW_1:3; :: thesis: for z9 being Element of B_6 st x <= z9 & y <= z9 holds

z <= z9

let w be Element of B_6; :: thesis: ( x <= w & y <= w implies z <= w )

assume ( x <= w & y <= w ) ; :: thesis: z <= w

then ( x c= w & y c= w ) by YELLOW_1:3;

then x \/ y c= w by XBOOLE_1:8;

hence z <= w by YELLOW_1:3; :: thesis: verum

end;

( x <= z & y <= z & ( for z9 being Element of B_6 st x <= z9 & y <= z9 holds

z <= z9 ) )

take z ; :: thesis: ( x <= z & y <= z & ( for z9 being Element of B_6 st x <= z9 & y <= z9 holds

z <= z9 ) )

( x c= z & y c= z ) by XBOOLE_1:7;

hence ( x <= z & y <= z ) by YELLOW_1:3; :: thesis: for z9 being Element of B_6 st x <= z9 & y <= z9 holds

z <= z9

let w be Element of B_6; :: thesis: ( x <= w & y <= w implies z <= w )

assume ( x <= w & y <= w ) ; :: thesis: z <= w

then ( x c= w & y c= w ) by YELLOW_1:3;

then x \/ y c= w by XBOOLE_1:8;

hence z <= w by YELLOW_1:3; :: thesis: verum

proof

hence
( B_6 is with_suprema & B_6 is with_infima )
by A2; :: thesis: verum
let x, y be Element of B_6; :: according to LATTICE3:def 11 :: thesis: ex b_{1} being Element of the carrier of B_6 st

( b_{1} <= x & b_{1} <= y & ( for b_{2} being Element of the carrier of B_6 holds

( not b_{2} <= x or not b_{2} <= y or b_{2} <= b_{1} ) ) )

A68: {0,1,(3 \ 1),2,(3 \ 2),3} = the carrier of B_6 by YELLOW_1:1;

thus ex z being Element of B_6 st

( z <= x & z <= y & ( for z9 being Element of B_6 st z9 <= x & z9 <= y holds

z9 <= z ) ) :: thesis: verum

end;( b

( not b

A68: {0,1,(3 \ 1),2,(3 \ 2),3} = the carrier of B_6 by YELLOW_1:1;

thus ex z being Element of B_6 st

( z <= x & z <= y & ( for z9 being Element of B_6 st z9 <= x & z9 <= y holds

z9 <= z ) ) :: thesis: verum

proof
end;

per cases
( ( x = 0 & y = 0 ) or ( x = 0 & y = 3 \ 1 ) or ( x = 0 & y = 2 ) or ( x = 0 & y = 3 \ 2 ) or ( x = 0 & y = 3 ) or ( x = 3 \ 1 & y = 0 ) or ( x = 3 \ 1 & y = 3 \ 1 ) or ( x = 3 \ 1 & y = 2 ) or ( x = 1 & y = 0 ) or ( x = 1 & y = 1 ) or ( x = 1 & y = 3 \ 1 ) or ( x = 1 & y = 3 \ 2 ) or ( x = 1 & y = 3 ) or ( x = 1 & y = 2 ) or ( y = 1 & x = 0 ) or ( y = 1 & x = 1 ) or ( y = 1 & x = 3 \ 1 ) or ( y = 1 & x = 3 \ 2 ) or ( y = 1 & x = 3 ) or ( y = 1 & x = 2 ) or ( x = 3 \ 1 & y = 3 \ 2 ) or ( x = 3 \ 1 & y = 3 ) or ( x = 2 & y = 0 ) or ( x = 2 & y = 3 \ 1 ) or ( x = 2 & y = 2 ) or ( x = 2 & y = 3 \ 2 ) or ( x = 2 & y = 3 ) or ( x = 3 \ 2 & y = 0 ) or ( x = 3 \ 2 & y = 3 \ 1 ) or ( x = 3 \ 2 & y = 2 ) or ( x = 3 \ 2 & y = 3 \ 2 ) or ( x = 3 \ 2 & y = 3 ) or ( x = 3 & y = 0 ) or ( x = 3 & y = 3 \ 1 ) or ( x = 3 & y = 2 ) or ( x = 3 & y = 3 \ 2 ) or ( x = 3 & y = 3 ) )
by A68, ENUMSET1:def 4;

end;

suppose
( x = 0 & y = 0 )
; :: thesis: ex z being Element of B_6 st

( z <= x & z <= y & ( for z9 being Element of B_6 st z9 <= x & z9 <= y holds

z9 <= z ) )

( z <= x & z <= y & ( for z9 being Element of B_6 st z9 <= x & z9 <= y holds

z9 <= z ) )

then reconsider z = x /\ y as Element of B_6 ;

take z ; :: thesis: ( z <= x & z <= y & ( for z9 being Element of B_6 st z9 <= x & z9 <= y holds

z9 <= z ) )

( z c= x & z c= y ) by XBOOLE_1:17;

hence ( z <= x & z <= y ) by YELLOW_1:3; :: thesis: for z9 being Element of B_6 st z9 <= x & z9 <= y holds

z9 <= z

let w be Element of B_6; :: thesis: ( w <= x & w <= y implies w <= z )

assume ( w <= x & w <= y ) ; :: thesis: w <= z

then ( w c= x & w c= y ) by YELLOW_1:3;

then w c= x /\ y by XBOOLE_1:19;

hence w <= z by YELLOW_1:3; :: thesis: verum

end;take z ; :: thesis: ( z <= x & z <= y & ( for z9 being Element of B_6 st z9 <= x & z9 <= y holds

z9 <= z ) )

( z c= x & z c= y ) by XBOOLE_1:17;

hence ( z <= x & z <= y ) by YELLOW_1:3; :: thesis: for z9 being Element of B_6 st z9 <= x & z9 <= y holds

z9 <= z

let w be Element of B_6; :: thesis: ( w <= x & w <= y implies w <= z )

assume ( w <= x & w <= y ) ; :: thesis: w <= z

then ( w c= x & w c= y ) by YELLOW_1:3;

then w c= x /\ y by XBOOLE_1:19;

hence w <= z by YELLOW_1:3; :: thesis: verum

suppose
( x = 0 & y = 3 \ 1 )
; :: thesis: ex z being Element of B_6 st

( z <= x & z <= y & ( for z9 being Element of B_6 st z9 <= x & z9 <= y holds

z9 <= z ) )

( z <= x & z <= y & ( for z9 being Element of B_6 st z9 <= x & z9 <= y holds

z9 <= z ) )

then reconsider z = x /\ y as Element of B_6 ;

take z ; :: thesis: ( z <= x & z <= y & ( for z9 being Element of B_6 st z9 <= x & z9 <= y holds

z9 <= z ) )

( z c= x & z c= y ) by XBOOLE_1:17;

hence ( z <= x & z <= y ) by YELLOW_1:3; :: thesis: for z9 being Element of B_6 st z9 <= x & z9 <= y holds

z9 <= z

let w be Element of B_6; :: thesis: ( w <= x & w <= y implies w <= z )

assume ( w <= x & w <= y ) ; :: thesis: w <= z

then ( w c= x & w c= y ) by YELLOW_1:3;

then w c= x /\ y by XBOOLE_1:19;

hence w <= z by YELLOW_1:3; :: thesis: verum

end;take z ; :: thesis: ( z <= x & z <= y & ( for z9 being Element of B_6 st z9 <= x & z9 <= y holds

z9 <= z ) )

( z c= x & z c= y ) by XBOOLE_1:17;

hence ( z <= x & z <= y ) by YELLOW_1:3; :: thesis: for z9 being Element of B_6 st z9 <= x & z9 <= y holds

z9 <= z

let w be Element of B_6; :: thesis: ( w <= x & w <= y implies w <= z )

assume ( w <= x & w <= y ) ; :: thesis: w <= z

then ( w c= x & w c= y ) by YELLOW_1:3;

then w c= x /\ y by XBOOLE_1:19;

hence w <= z by YELLOW_1:3; :: thesis: verum

suppose
( x = 0 & y = 2 )
; :: thesis: ex z being Element of B_6 st

( z <= x & z <= y & ( for z9 being Element of B_6 st z9 <= x & z9 <= y holds

z9 <= z ) )

( z <= x & z <= y & ( for z9 being Element of B_6 st z9 <= x & z9 <= y holds

z9 <= z ) )

then reconsider z = x /\ y as Element of B_6 ;

take z ; :: thesis: ( z <= x & z <= y & ( for z9 being Element of B_6 st z9 <= x & z9 <= y holds

z9 <= z ) )

( z c= x & z c= y ) by XBOOLE_1:17;

hence ( z <= x & z <= y ) by YELLOW_1:3; :: thesis: for z9 being Element of B_6 st z9 <= x & z9 <= y holds

z9 <= z

let w be Element of B_6; :: thesis: ( w <= x & w <= y implies w <= z )

assume ( w <= x & w <= y ) ; :: thesis: w <= z

then ( w c= x & w c= y ) by YELLOW_1:3;

then w c= x /\ y by XBOOLE_1:19;

hence w <= z by YELLOW_1:3; :: thesis: verum

end;take z ; :: thesis: ( z <= x & z <= y & ( for z9 being Element of B_6 st z9 <= x & z9 <= y holds

z9 <= z ) )

( z c= x & z c= y ) by XBOOLE_1:17;

hence ( z <= x & z <= y ) by YELLOW_1:3; :: thesis: for z9 being Element of B_6 st z9 <= x & z9 <= y holds

z9 <= z

let w be Element of B_6; :: thesis: ( w <= x & w <= y implies w <= z )

assume ( w <= x & w <= y ) ; :: thesis: w <= z

then ( w c= x & w c= y ) by YELLOW_1:3;

then w c= x /\ y by XBOOLE_1:19;

hence w <= z by YELLOW_1:3; :: thesis: verum

suppose
( x = 0 & y = 3 \ 2 )
; :: thesis: ex z being Element of B_6 st

( z <= x & z <= y & ( for z9 being Element of B_6 st z9 <= x & z9 <= y holds

z9 <= z ) )

then reconsider z = x /\ y as Element of B_6 ;

take z ; :: thesis: ( z <= x & z <= y & ( for z9 being Element of B_6 st z9 <= x & z9 <= y holds

z9 <= z ) )

( z c= x & z c= y ) by XBOOLE_1:17;

hence ( z <= x & z <= y ) by YELLOW_1:3; :: thesis: for z9 being Element of B_6 st z9 <= x & z9 <= y holds

z9 <= z

let w be Element of B_6; :: thesis: ( w <= x & w <= y implies w <= z )

assume ( w <= x & w <= y ) ; :: thesis: w <= z

then ( w c= x & w c= y ) by YELLOW_1:3;

then w c= x /\ y by XBOOLE_1:19;

hence w <= z by YELLOW_1:3; :: thesis: verum

end;

( z <= x & z <= y & ( for z9 being Element of B_6 st z9 <= x & z9 <= y holds

z9 <= z ) )

take z ; :: thesis: ( z <= x & z <= y & ( for z9 being Element of B_6 st z9 <= x & z9 <= y holds

z9 <= z ) )

( z c= x & z c= y ) by XBOOLE_1:17;

hence ( z <= x & z <= y ) by YELLOW_1:3; :: thesis: for z9 being Element of B_6 st z9 <= x & z9 <= y holds

z9 <= z

let w be Element of B_6; :: thesis: ( w <= x & w <= y implies w <= z )

assume ( w <= x & w <= y ) ; :: thesis: w <= z

then ( w c= x & w c= y ) by YELLOW_1:3;

then w c= x /\ y by XBOOLE_1:19;

hence w <= z by YELLOW_1:3; :: thesis: verum

suppose
( x = 0 & y = 3 )
; :: thesis: ex z being Element of B_6 st

( z <= x & z <= y & ( for z9 being Element of B_6 st z9 <= x & z9 <= y holds

z9 <= z ) )

then reconsider z = x /\ y as Element of B_6 ;

take z ; :: thesis: ( z <= x & z <= y & ( for z9 being Element of B_6 st z9 <= x & z9 <= y holds

z9 <= z ) )

( z c= x & z c= y ) by XBOOLE_1:17;

hence ( z <= x & z <= y ) by YELLOW_1:3; :: thesis: for z9 being Element of B_6 st z9 <= x & z9 <= y holds

z9 <= z

let w be Element of B_6; :: thesis: ( w <= x & w <= y implies w <= z )

assume ( w <= x & w <= y ) ; :: thesis: w <= z

then ( w c= x & w c= y ) by YELLOW_1:3;

then w c= x /\ y by XBOOLE_1:19;

hence w <= z by YELLOW_1:3; :: thesis: verum

end;

( z <= x & z <= y & ( for z9 being Element of B_6 st z9 <= x & z9 <= y holds

z9 <= z ) )

take z ; :: thesis: ( z <= x & z <= y & ( for z9 being Element of B_6 st z9 <= x & z9 <= y holds

z9 <= z ) )

( z c= x & z c= y ) by XBOOLE_1:17;

hence ( z <= x & z <= y ) by YELLOW_1:3; :: thesis: for z9 being Element of B_6 st z9 <= x & z9 <= y holds

z9 <= z

let w be Element of B_6; :: thesis: ( w <= x & w <= y implies w <= z )

assume ( w <= x & w <= y ) ; :: thesis: w <= z

then ( w c= x & w c= y ) by YELLOW_1:3;

then w c= x /\ y by XBOOLE_1:19;

hence w <= z by YELLOW_1:3; :: thesis: verum

suppose
( x = 3 \ 1 & y = 0 )
; :: thesis: ex z being Element of B_6 st

( z <= x & z <= y & ( for z9 being Element of B_6 st z9 <= x & z9 <= y holds

z9 <= z ) )

then reconsider z = x /\ y as Element of B_6 ;

take z ; :: thesis: ( z <= x & z <= y & ( for z9 being Element of B_6 st z9 <= x & z9 <= y holds

z9 <= z ) )

( z c= x & z c= y ) by XBOOLE_1:17;

hence ( z <= x & z <= y ) by YELLOW_1:3; :: thesis: for z9 being Element of B_6 st z9 <= x & z9 <= y holds

z9 <= z

let w be Element of B_6; :: thesis: ( w <= x & w <= y implies w <= z )

assume ( w <= x & w <= y ) ; :: thesis: w <= z

then ( w c= x & w c= y ) by YELLOW_1:3;

then w c= x /\ y by XBOOLE_1:19;

hence w <= z by YELLOW_1:3; :: thesis: verum

end;

( z <= x & z <= y & ( for z9 being Element of B_6 st z9 <= x & z9 <= y holds

z9 <= z ) )

take z ; :: thesis: ( z <= x & z <= y & ( for z9 being Element of B_6 st z9 <= x & z9 <= y holds

z9 <= z ) )

( z c= x & z c= y ) by XBOOLE_1:17;

hence ( z <= x & z <= y ) by YELLOW_1:3; :: thesis: for z9 being Element of B_6 st z9 <= x & z9 <= y holds

z9 <= z

let w be Element of B_6; :: thesis: ( w <= x & w <= y implies w <= z )

assume ( w <= x & w <= y ) ; :: thesis: w <= z

then ( w c= x & w c= y ) by YELLOW_1:3;

then w c= x /\ y by XBOOLE_1:19;

hence w <= z by YELLOW_1:3; :: thesis: verum

suppose
( x = 3 \ 1 & y = 3 \ 1 )
; :: thesis: ex z being Element of B_6 st

( z <= x & z <= y & ( for z9 being Element of B_6 st z9 <= x & z9 <= y holds

z9 <= z ) )

then reconsider z = x /\ y as Element of B_6 ;

take z ; :: thesis: ( z <= x & z <= y & ( for z9 being Element of B_6 st z9 <= x & z9 <= y holds

z9 <= z ) )

( z c= x & z c= y ) by XBOOLE_1:17;

hence ( z <= x & z <= y ) by YELLOW_1:3; :: thesis: for z9 being Element of B_6 st z9 <= x & z9 <= y holds

z9 <= z

let w be Element of B_6; :: thesis: ( w <= x & w <= y implies w <= z )

assume ( w <= x & w <= y ) ; :: thesis: w <= z

then ( w c= x & w c= y ) by YELLOW_1:3;

then w c= x /\ y by XBOOLE_1:19;

hence w <= z by YELLOW_1:3; :: thesis: verum

end;

( z <= x & z <= y & ( for z9 being Element of B_6 st z9 <= x & z9 <= y holds

z9 <= z ) )

take z ; :: thesis: ( z <= x & z <= y & ( for z9 being Element of B_6 st z9 <= x & z9 <= y holds

z9 <= z ) )

( z c= x & z c= y ) by XBOOLE_1:17;

hence ( z <= x & z <= y ) by YELLOW_1:3; :: thesis: for z9 being Element of B_6 st z9 <= x & z9 <= y holds

z9 <= z

let w be Element of B_6; :: thesis: ( w <= x & w <= y implies w <= z )

assume ( w <= x & w <= y ) ; :: thesis: w <= z

then ( w c= x & w c= y ) by YELLOW_1:3;

then w c= x /\ y by XBOOLE_1:19;

hence w <= z by YELLOW_1:3; :: thesis: verum

suppose A69:
( x = 3 \ 1 & y = 2 )
; :: thesis: ex z being Element of B_6 st

( z <= x & z <= y & ( for z9 being Element of B_6 st z9 <= x & z9 <= y holds

z9 <= z ) )

( z <= x & z <= y & ( for z9 being Element of B_6 st z9 <= x & z9 <= y holds

z9 <= z ) )

0 in {0,1,(3 \ 1),2,(3 \ 2),3}
by ENUMSET1:def 4;

then reconsider z = 0 as Element of B_6 by YELLOW_1:1;

take z ; :: thesis: ( z <= x & z <= y & ( for z9 being Element of B_6 st z9 <= x & z9 <= y holds

z9 <= z ) )

( z c= x & z c= y ) ;

hence ( z <= x & z <= y ) by YELLOW_1:3; :: thesis: for z9 being Element of B_6 st z9 <= x & z9 <= y holds

z9 <= z

let z9 be Element of B_6; :: thesis: ( z9 <= x & z9 <= y implies z9 <= z )

assume that

A70: z9 <= x and

A71: z9 <= y ; :: thesis: z9 <= z

A72: z9 c= 3 \ 1 by A69, A70, YELLOW_1:3;

hence z9 <= z by A75, A73, A79, A81, A77, ENUMSET1:def 4; :: thesis: verum

end;then reconsider z = 0 as Element of B_6 by YELLOW_1:1;

take z ; :: thesis: ( z <= x & z <= y & ( for z9 being Element of B_6 st z9 <= x & z9 <= y holds

z9 <= z ) )

( z c= x & z c= y ) ;

hence ( z <= x & z <= y ) by YELLOW_1:3; :: thesis: for z9 being Element of B_6 st z9 <= x & z9 <= y holds

z9 <= z

let z9 be Element of B_6; :: thesis: ( z9 <= x & z9 <= y implies z9 <= z )

assume that

A70: z9 <= x and

A71: z9 <= y ; :: thesis: z9 <= z

A72: z9 c= 3 \ 1 by A69, A70, YELLOW_1:3;

A73: now :: thesis: not z9 = 2

A74:
z9 c= 2
by A69, A71, YELLOW_1:3;assume
z9 = 2
; :: thesis: contradiction

then 0 in z9 by CARD_1:50, TARSKI:def 2;

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

end;then 0 in z9 by CARD_1:50, TARSKI:def 2;

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

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

assume
z9 = 3 \ 1
; :: thesis: contradiction

then A76: 2 in z9 by TARSKI:def 2, YELLOW11:3;

not 2 in 2 ;

hence contradiction by A74, A76; :: thesis: verum

end;then A76: 2 in z9 by TARSKI:def 2, YELLOW11:3;

not 2 in 2 ;

hence contradiction by A74, A76; :: thesis: verum

A77: now :: thesis: not z9 = 3

assume
z9 = 3
; :: thesis: contradiction

then A78: 2 in z9 by CARD_1:51, ENUMSET1:def 1;

not 2 in 2 ;

hence contradiction by A74, A78; :: thesis: verum

end;then A78: 2 in z9 by CARD_1:51, ENUMSET1:def 1;

not 2 in 2 ;

hence contradiction by A74, A78; :: thesis: verum

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

assume
z9 = 3 \ 2
; :: thesis: contradiction

then A80: 2 in z9 by TARSKI:def 1, YELLOW11:4;

not 2 in 2 ;

hence contradiction by A74, A80; :: thesis: verum

end;then A80: 2 in z9 by TARSKI:def 1, YELLOW11:4;

not 2 in 2 ;

hence contradiction by A74, A80; :: thesis: verum

A81: now :: thesis: not z9 = 1

z9 is Element of {0,1,(3 \ 1),2,(3 \ 2),3}
by YELLOW_1:1;assume
z9 = 1
; :: thesis: contradiction

then 0 in z9 by CARD_1:49, TARSKI:def 1;

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

end;then 0 in z9 by CARD_1:49, TARSKI:def 1;

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

hence z9 <= z by A75, A73, A79, A81, A77, ENUMSET1:def 4; :: thesis: verum

suppose
( x = 1 & y = 0 )
; :: thesis: ex z being Element of B_6 st

( z <= x & z <= y & ( for z9 being Element of B_6 st z9 <= x & z9 <= y holds

z9 <= z ) )

then reconsider z = x /\ y as Element of B_6 ;

take z ; :: thesis: ( z <= x & z <= y & ( for z9 being Element of B_6 st z9 <= x & z9 <= y holds

z9 <= z ) )

( z c= x & z c= y ) by XBOOLE_1:17;

hence ( z <= x & z <= y ) by YELLOW_1:3; :: thesis: for z9 being Element of B_6 st z9 <= x & z9 <= y holds

z9 <= z

let w be Element of B_6; :: thesis: ( w <= x & w <= y implies w <= z )

assume ( w <= x & w <= y ) ; :: thesis: w <= z

then ( w c= x & w c= y ) by YELLOW_1:3;

then w c= x /\ y by XBOOLE_1:19;

hence w <= z by YELLOW_1:3; :: thesis: verum

end;

( z <= x & z <= y & ( for z9 being Element of B_6 st z9 <= x & z9 <= y holds

z9 <= z ) )

take z ; :: thesis: ( z <= x & z <= y & ( for z9 being Element of B_6 st z9 <= x & z9 <= y holds

z9 <= z ) )

( z c= x & z c= y ) by XBOOLE_1:17;

hence ( z <= x & z <= y ) by YELLOW_1:3; :: thesis: for z9 being Element of B_6 st z9 <= x & z9 <= y holds

z9 <= z

let w be Element of B_6; :: thesis: ( w <= x & w <= y implies w <= z )

assume ( w <= x & w <= y ) ; :: thesis: w <= z

then ( w c= x & w c= y ) by YELLOW_1:3;

then w c= x /\ y by XBOOLE_1:19;

hence w <= z by YELLOW_1:3; :: thesis: verum

suppose
( x = 1 & y = 1 )
; :: thesis: ex z being Element of B_6 st

( z <= x & z <= y & ( for z9 being Element of B_6 st z9 <= x & z9 <= y holds

z9 <= z ) )

then reconsider z = x /\ y as Element of B_6 ;

take z ; :: thesis: ( z <= x & z <= y & ( for z9 being Element of B_6 st z9 <= x & z9 <= y holds

z9 <= z ) )

( z c= x & z c= y ) by XBOOLE_1:17;

hence ( z <= x & z <= y ) by YELLOW_1:3; :: thesis: for z9 being Element of B_6 st z9 <= x & z9 <= y holds

z9 <= z

let w be Element of B_6; :: thesis: ( w <= x & w <= y implies w <= z )

assume ( w <= x & w <= y ) ; :: thesis: w <= z

then ( w c= x & w c= y ) by YELLOW_1:3;

then w c= x /\ y by XBOOLE_1:19;

hence w <= z by YELLOW_1:3; :: thesis: verum

end;

( z <= x & z <= y & ( for z9 being Element of B_6 st z9 <= x & z9 <= y holds

z9 <= z ) )

take z ; :: thesis: ( z <= x & z <= y & ( for z9 being Element of B_6 st z9 <= x & z9 <= y holds

z9 <= z ) )

( z c= x & z c= y ) by XBOOLE_1:17;

hence ( z <= x & z <= y ) by YELLOW_1:3; :: thesis: for z9 being Element of B_6 st z9 <= x & z9 <= y holds

z9 <= z

let w be Element of B_6; :: thesis: ( w <= x & w <= y implies w <= z )

assume ( w <= x & w <= y ) ; :: thesis: w <= z

then ( w c= x & w c= y ) by YELLOW_1:3;

then w c= x /\ y by XBOOLE_1:19;

hence w <= z by YELLOW_1:3; :: thesis: verum

suppose
( x = 1 & y = 3 \ 1 )
; :: thesis: ex z being Element of B_6 st

( z <= x & z <= y & ( for z9 being Element of B_6 st z9 <= x & z9 <= y holds

z9 <= z ) )

( z <= x & z <= y & ( for z9 being Element of B_6 st z9 <= x & z9 <= y holds

z9 <= z ) )

then
x misses y
by XBOOLE_1:79;

then x /\ y = 0 by XBOOLE_0:def 7;

then reconsider z = x /\ y as Element of B_6 by A1, ENUMSET1:def 4;

take z ; :: thesis: ( z <= x & z <= y & ( for z9 being Element of B_6 st z9 <= x & z9 <= y holds

z9 <= z ) )

( z c= x & z c= y ) by XBOOLE_1:17;

hence ( z <= x & z <= y ) by YELLOW_1:3; :: thesis: for z9 being Element of B_6 st z9 <= x & z9 <= y holds

z9 <= z

let w be Element of B_6; :: thesis: ( w <= x & w <= y implies w <= z )

assume ( w <= x & w <= y ) ; :: thesis: w <= z

then ( w c= x & w c= y ) by YELLOW_1:3;

then w c= x /\ y by XBOOLE_1:19;

hence w <= z by YELLOW_1:3; :: thesis: verum

end;then x /\ y = 0 by XBOOLE_0:def 7;

then reconsider z = x /\ y as Element of B_6 by A1, ENUMSET1:def 4;

take z ; :: thesis: ( z <= x & z <= y & ( for z9 being Element of B_6 st z9 <= x & z9 <= y holds

z9 <= z ) )

( z c= x & z c= y ) by XBOOLE_1:17;

hence ( z <= x & z <= y ) by YELLOW_1:3; :: thesis: for z9 being Element of B_6 st z9 <= x & z9 <= y holds

z9 <= z

let w be Element of B_6; :: thesis: ( w <= x & w <= y implies w <= z )

assume ( w <= x & w <= y ) ; :: thesis: w <= z

then ( w c= x & w c= y ) by YELLOW_1:3;

then w c= x /\ y by XBOOLE_1:19;

hence w <= z by YELLOW_1:3; :: thesis: verum

suppose
( x = 1 & y = 3 \ 2 )
; :: thesis: ex z being Element of B_6 st

( z <= x & z <= y & ( for z9 being Element of B_6 st z9 <= x & z9 <= y holds

z9 <= z ) )

( z <= x & z <= y & ( for z9 being Element of B_6 st z9 <= x & z9 <= y holds

z9 <= z ) )

then
x /\ y = 0
by Lm3, XBOOLE_0:def 7;

then reconsider z = x /\ y as Element of B_6 by A1, ENUMSET1:def 4;

take z ; :: thesis: ( z <= x & z <= y & ( for z9 being Element of B_6 st z9 <= x & z9 <= y holds

z9 <= z ) )

( z c= x & z c= y ) by XBOOLE_1:17;

hence ( z <= x & z <= y ) by YELLOW_1:3; :: thesis: for z9 being Element of B_6 st z9 <= x & z9 <= y holds

z9 <= z

let w be Element of B_6; :: thesis: ( w <= x & w <= y implies w <= z )

assume ( w <= x & w <= y ) ; :: thesis: w <= z

then ( w c= x & w c= y ) by YELLOW_1:3;

then w c= x /\ y by XBOOLE_1:19;

hence w <= z by YELLOW_1:3; :: thesis: verum

end;then reconsider z = x /\ y as Element of B_6 by A1, ENUMSET1:def 4;

take z ; :: thesis: ( z <= x & z <= y & ( for z9 being Element of B_6 st z9 <= x & z9 <= y holds

z9 <= z ) )

( z c= x & z c= y ) by XBOOLE_1:17;

hence ( z <= x & z <= y ) by YELLOW_1:3; :: thesis: for z9 being Element of B_6 st z9 <= x & z9 <= y holds

z9 <= z

let w be Element of B_6; :: thesis: ( w <= x & w <= y implies w <= z )

assume ( w <= x & w <= y ) ; :: thesis: w <= z

then ( w c= x & w c= y ) by YELLOW_1:3;

then w c= x /\ y by XBOOLE_1:19;

hence w <= z by YELLOW_1:3; :: thesis: verum

suppose A82:
( x = 1 & y = 3 )
; :: thesis: ex z being Element of B_6 st

( z <= x & z <= y & ( for z9 being Element of B_6 st z9 <= x & z9 <= y holds

z9 <= z ) )

( z <= x & z <= y & ( for z9 being Element of B_6 st z9 <= x & z9 <= y holds

z9 <= z ) )

Segm 1 c= Segm 3
by NAT_1:39;

then reconsider z = x /\ y as Element of B_6 by A82, XBOOLE_1:28;

take z ; :: thesis: ( z <= x & z <= y & ( for z9 being Element of B_6 st z9 <= x & z9 <= y holds

z9 <= z ) )

( z c= x & z c= y ) by XBOOLE_1:17;

hence ( z <= x & z <= y ) by YELLOW_1:3; :: thesis: for z9 being Element of B_6 st z9 <= x & z9 <= y holds

z9 <= z

let w be Element of B_6; :: thesis: ( w <= x & w <= y implies w <= z )

assume ( w <= x & w <= y ) ; :: thesis: w <= z

then ( w c= x & w c= y ) by YELLOW_1:3;

then w c= x /\ y by XBOOLE_1:19;

hence w <= z by YELLOW_1:3; :: thesis: verum

end;then reconsider z = x /\ y as Element of B_6 by A82, XBOOLE_1:28;

take z ; :: thesis: ( z <= x & z <= y & ( for z9 being Element of B_6 st z9 <= x & z9 <= y holds

z9 <= z ) )

( z c= x & z c= y ) by XBOOLE_1:17;

hence ( z <= x & z <= y ) by YELLOW_1:3; :: thesis: for z9 being Element of B_6 st z9 <= x & z9 <= y holds

z9 <= z

let w be Element of B_6; :: thesis: ( w <= x & w <= y implies w <= z )

assume ( w <= x & w <= y ) ; :: thesis: w <= z

then ( w c= x & w c= y ) by YELLOW_1:3;

then w c= x /\ y by XBOOLE_1:19;

hence w <= z by YELLOW_1:3; :: thesis: verum

suppose
( x = 1 & y = 2 )
; :: thesis: ex z being Element of B_6 st

( z <= x & z <= y & ( for z9 being Element of B_6 st z9 <= x & z9 <= y holds

z9 <= z ) )

( z <= x & z <= y & ( for z9 being Element of B_6 st z9 <= x & z9 <= y holds

z9 <= z ) )

then reconsider z = x /\ y as Element of B_6 by CARD_1:49, CARD_1:50, ZFMISC_1:13;

take z ; :: thesis: ( z <= x & z <= y & ( for z9 being Element of B_6 st z9 <= x & z9 <= y holds

z9 <= z ) )

( z c= x & z c= y ) by XBOOLE_1:17;

hence ( z <= x & z <= y ) by YELLOW_1:3; :: thesis: for z9 being Element of B_6 st z9 <= x & z9 <= y holds

z9 <= z

let w be Element of B_6; :: thesis: ( w <= x & w <= y implies w <= z )

assume ( w <= x & w <= y ) ; :: thesis: w <= z

then ( w c= x & w c= y ) by YELLOW_1:3;

then w c= x /\ y by XBOOLE_1:19;

hence w <= z by YELLOW_1:3; :: thesis: verum

end;take z ; :: thesis: ( z <= x & z <= y & ( for z9 being Element of B_6 st z9 <= x & z9 <= y holds

z9 <= z ) )

( z c= x & z c= y ) by XBOOLE_1:17;

hence ( z <= x & z <= y ) by YELLOW_1:3; :: thesis: for z9 being Element of B_6 st z9 <= x & z9 <= y holds

z9 <= z

let w be Element of B_6; :: thesis: ( w <= x & w <= y implies w <= z )

assume ( w <= x & w <= y ) ; :: thesis: w <= z

then ( w c= x & w c= y ) by YELLOW_1:3;

then w c= x /\ y by XBOOLE_1:19;

hence w <= z by YELLOW_1:3; :: thesis: verum

suppose
( y = 1 & x = 0 )
; :: thesis: ex z being Element of B_6 st

( z <= x & z <= y & ( for z9 being Element of B_6 st z9 <= x & z9 <= y holds

z9 <= z ) )

then reconsider z = x /\ y as Element of B_6 ;

take z ; :: thesis: ( z <= x & z <= y & ( for z9 being Element of B_6 st z9 <= x & z9 <= y holds

z9 <= z ) )

( z c= x & z c= y ) by XBOOLE_1:17;

hence ( z <= x & z <= y ) by YELLOW_1:3; :: thesis: for z9 being Element of B_6 st z9 <= x & z9 <= y holds

z9 <= z

let w be Element of B_6; :: thesis: ( w <= x & w <= y implies w <= z )

assume ( w <= x & w <= y ) ; :: thesis: w <= z

then ( w c= x & w c= y ) by YELLOW_1:3;

then w c= x /\ y by XBOOLE_1:19;

hence w <= z by YELLOW_1:3; :: thesis: verum

end;

( z <= x & z <= y & ( for z9 being Element of B_6 st z9 <= x & z9 <= y holds

z9 <= z ) )

take z ; :: thesis: ( z <= x & z <= y & ( for z9 being Element of B_6 st z9 <= x & z9 <= y holds

z9 <= z ) )

( z c= x & z c= y ) by XBOOLE_1:17;

hence ( z <= x & z <= y ) by YELLOW_1:3; :: thesis: for z9 being Element of B_6 st z9 <= x & z9 <= y holds

z9 <= z

let w be Element of B_6; :: thesis: ( w <= x & w <= y implies w <= z )

assume ( w <= x & w <= y ) ; :: thesis: w <= z

then ( w c= x & w c= y ) by YELLOW_1:3;

then w c= x /\ y by XBOOLE_1:19;

hence w <= z by YELLOW_1:3; :: thesis: verum

suppose
( y = 1 & x = 1 )
; :: thesis: ex z being Element of B_6 st

( z <= x & z <= y & ( for z9 being Element of B_6 st z9 <= x & z9 <= y holds

z9 <= z ) )

then reconsider z = x /\ y as Element of B_6 ;

take z ; :: thesis: ( z <= x & z <= y & ( for z9 being Element of B_6 st z9 <= x & z9 <= y holds

z9 <= z ) )

( z c= x & z c= y ) by XBOOLE_1:17;

hence ( z <= x & z <= y ) by YELLOW_1:3; :: thesis: for z9 being Element of B_6 st z9 <= x & z9 <= y holds

z9 <= z

let w be Element of B_6; :: thesis: ( w <= x & w <= y implies w <= z )

assume ( w <= x & w <= y ) ; :: thesis: w <= z

then ( w c= x & w c= y ) by YELLOW_1:3;

then w c= x /\ y by XBOOLE_1:19;

hence w <= z by YELLOW_1:3; :: thesis: verum

end;

( z <= x & z <= y & ( for z9 being Element of B_6 st z9 <= x & z9 <= y holds

z9 <= z ) )

take z ; :: thesis: ( z <= x & z <= y & ( for z9 being Element of B_6 st z9 <= x & z9 <= y holds

z9 <= z ) )

( z c= x & z c= y ) by XBOOLE_1:17;

hence ( z <= x & z <= y ) by YELLOW_1:3; :: thesis: for z9 being Element of B_6 st z9 <= x & z9 <= y holds

z9 <= z

let w be Element of B_6; :: thesis: ( w <= x & w <= y implies w <= z )

assume ( w <= x & w <= y ) ; :: thesis: w <= z

then ( w c= x & w c= y ) by YELLOW_1:3;

then w c= x /\ y by XBOOLE_1:19;

hence w <= z by YELLOW_1:3; :: thesis: verum

suppose
( y = 1 & x = 3 \ 1 )
; :: thesis: ex z being Element of B_6 st

( z <= x & z <= y & ( for z9 being Element of B_6 st z9 <= x & z9 <= y holds

z9 <= z ) )

( z <= x & z <= y & ( for z9 being Element of B_6 st z9 <= x & z9 <= y holds

z9 <= z ) )

then
x misses y
by XBOOLE_1:79;

then x /\ y = 0 by XBOOLE_0:def 7;

then reconsider z = x /\ y as Element of B_6 by A1, ENUMSET1:def 4;

take z ; :: thesis: ( z <= x & z <= y & ( for z9 being Element of B_6 st z9 <= x & z9 <= y holds

z9 <= z ) )

( z c= x & z c= y ) by XBOOLE_1:17;

hence ( z <= x & z <= y ) by YELLOW_1:3; :: thesis: for z9 being Element of B_6 st z9 <= x & z9 <= y holds

z9 <= z

let w be Element of B_6; :: thesis: ( w <= x & w <= y implies w <= z )

assume ( w <= x & w <= y ) ; :: thesis: w <= z

then ( w c= x & w c= y ) by YELLOW_1:3;

then w c= x /\ y by XBOOLE_1:19;

hence w <= z by YELLOW_1:3; :: thesis: verum

end;then x /\ y = 0 by XBOOLE_0:def 7;

then reconsider z = x /\ y as Element of B_6 by A1, ENUMSET1:def 4;

take z ; :: thesis: ( z <= x & z <= y & ( for z9 being Element of B_6 st z9 <= x & z9 <= y holds

z9 <= z ) )

( z c= x & z c= y ) by XBOOLE_1:17;

hence ( z <= x & z <= y ) by YELLOW_1:3; :: thesis: for z9 being Element of B_6 st z9 <= x & z9 <= y holds

z9 <= z

let w be Element of B_6; :: thesis: ( w <= x & w <= y implies w <= z )

assume ( w <= x & w <= y ) ; :: thesis: w <= z

then ( w c= x & w c= y ) by YELLOW_1:3;

then w c= x /\ y by XBOOLE_1:19;

hence w <= z by YELLOW_1:3; :: thesis: verum

suppose
( y = 1 & x = 3 \ 2 )
; :: thesis: ex z being Element of B_6 st

( z <= x & z <= y & ( for z9 being Element of B_6 st z9 <= x & z9 <= y holds

z9 <= z ) )

( z <= x & z <= y & ( for z9 being Element of B_6 st z9 <= x & z9 <= y holds

z9 <= z ) )

then
x /\ y = {}
by Lm3, XBOOLE_0:def 7;

then reconsider z = x /\ y as Element of B_6 by A1, ENUMSET1:def 4;

take z ; :: thesis: ( z <= x & z <= y & ( for z9 being Element of B_6 st z9 <= x & z9 <= y holds

z9 <= z ) )

( z c= x & z c= y ) by XBOOLE_1:17;

hence ( z <= x & z <= y ) by YELLOW_1:3; :: thesis: for z9 being Element of B_6 st z9 <= x & z9 <= y holds

z9 <= z

let w be Element of B_6; :: thesis: ( w <= x & w <= y implies w <= z )

assume ( w <= x & w <= y ) ; :: thesis: w <= z

then ( w c= x & w c= y ) by YELLOW_1:3;

then w c= x /\ y by XBOOLE_1:19;

hence w <= z by YELLOW_1:3; :: thesis: verum

end;then reconsider z = x /\ y as Element of B_6 by A1, ENUMSET1:def 4;

take z ; :: thesis: ( z <= x & z <= y & ( for z9 being Element of B_6 st z9 <= x & z9 <= y holds

z9 <= z ) )

( z c= x & z c= y ) by XBOOLE_1:17;

hence ( z <= x & z <= y ) by YELLOW_1:3; :: thesis: for z9 being Element of B_6 st z9 <= x & z9 <= y holds

z9 <= z

let w be Element of B_6; :: thesis: ( w <= x & w <= y implies w <= z )

assume ( w <= x & w <= y ) ; :: thesis: w <= z

then ( w c= x & w c= y ) by YELLOW_1:3;

then w c= x /\ y by XBOOLE_1:19;

hence w <= z by YELLOW_1:3; :: thesis: verum

suppose A83:
( y = 1 & x = 3 )
; :: thesis: ex z being Element of B_6 st

( z <= x & z <= y & ( for z9 being Element of B_6 st z9 <= x & z9 <= y holds

z9 <= z ) )

( z <= x & z <= y & ( for z9 being Element of B_6 st z9 <= x & z9 <= y holds

z9 <= z ) )

Segm 1 c= Segm 3
by NAT_1:39;

then reconsider z = x /\ y as Element of B_6 by A83, XBOOLE_1:28;

take z ; :: thesis: ( z <= x & z <= y & ( for z9 being Element of B_6 st z9 <= x & z9 <= y holds

z9 <= z ) )

( z c= x & z c= y ) by XBOOLE_1:17;

hence ( z <= x & z <= y ) by YELLOW_1:3; :: thesis: for z9 being Element of B_6 st z9 <= x & z9 <= y holds

z9 <= z

let w be Element of B_6; :: thesis: ( w <= x & w <= y implies w <= z )

assume ( w <= x & w <= y ) ; :: thesis: w <= z

then ( w c= x & w c= y ) by YELLOW_1:3;

then w c= x /\ y by XBOOLE_1:19;

hence w <= z by YELLOW_1:3; :: thesis: verum

end;then reconsider z = x /\ y as Element of B_6 by A83, XBOOLE_1:28;

take z ; :: thesis: ( z <= x & z <= y & ( for z9 being Element of B_6 st z9 <= x & z9 <= y holds

z9 <= z ) )

( z c= x & z c= y ) by XBOOLE_1:17;

hence ( z <= x & z <= y ) by YELLOW_1:3; :: thesis: for z9 being Element of B_6 st z9 <= x & z9 <= y holds

z9 <= z

let w be Element of B_6; :: thesis: ( w <= x & w <= y implies w <= z )

assume ( w <= x & w <= y ) ; :: thesis: w <= z

then ( w c= x & w c= y ) by YELLOW_1:3;

then w c= x /\ y by XBOOLE_1:19;

hence w <= z by YELLOW_1:3; :: thesis: verum

suppose
( y = 1 & x = 2 )
; :: thesis: ex z being Element of B_6 st

( z <= x & z <= y & ( for z9 being Element of B_6 st z9 <= x & z9 <= y holds

z9 <= z ) )

( z <= x & z <= y & ( for z9 being Element of B_6 st z9 <= x & z9 <= y holds

z9 <= z ) )

then reconsider z = x /\ y as Element of B_6 by CARD_1:49, CARD_1:50, ZFMISC_1:13;

take z ; :: thesis: ( z <= x & z <= y & ( for z9 being Element of B_6 st z9 <= x & z9 <= y holds

z9 <= z ) )

( z c= x & z c= y ) by XBOOLE_1:17;

hence ( z <= x & z <= y ) by YELLOW_1:3; :: thesis: for z9 being Element of B_6 st z9 <= x & z9 <= y holds

z9 <= z

let w be Element of B_6; :: thesis: ( w <= x & w <= y implies w <= z )

assume ( w <= x & w <= y ) ; :: thesis: w <= z

then ( w c= x & w c= y ) by YELLOW_1:3;

then w c= x /\ y by XBOOLE_1:19;

hence w <= z by YELLOW_1:3; :: thesis: verum

end;take z ; :: thesis: ( z <= x & z <= y & ( for z9 being Element of B_6 st z9 <= x & z9 <= y holds

z9 <= z ) )

( z c= x & z c= y ) by XBOOLE_1:17;

hence ( z <= x & z <= y ) by YELLOW_1:3; :: thesis: for z9 being Element of B_6 st z9 <= x & z9 <= y holds

z9 <= z

let w be Element of B_6; :: thesis: ( w <= x & w <= y implies w <= z )

assume ( w <= x & w <= y ) ; :: thesis: w <= z

then ( w c= x & w c= y ) by YELLOW_1:3;

then w c= x /\ y by XBOOLE_1:19;

hence w <= z by YELLOW_1:3; :: thesis: verum

suppose
( x = 3 \ 1 & y = 3 \ 2 )
; :: thesis: ex z being Element of B_6 st

( z <= x & z <= y & ( for z9 being Element of B_6 st z9 <= x & z9 <= y holds

z9 <= z ) )

( z <= x & z <= y & ( for z9 being Element of B_6 st z9 <= x & z9 <= y holds

z9 <= z ) )

then reconsider z = x /\ y as Element of B_6 by YELLOW11:3, YELLOW11:4, ZFMISC_1:13;

take z ; :: thesis: ( z <= x & z <= y & ( for z9 being Element of B_6 st z9 <= x & z9 <= y holds

z9 <= z ) )

( z c= x & z c= y ) by XBOOLE_1:17;

hence ( z <= x & z <= y ) by YELLOW_1:3; :: thesis: for z9 being Element of B_6 st z9 <= x & z9 <= y holds

z9 <= z

let w be Element of B_6; :: thesis: ( w <= x & w <= y implies w <= z )

assume ( w <= x & w <= y ) ; :: thesis: w <= z

then ( w c= x & w c= y ) by YELLOW_1:3;

then w c= x /\ y by XBOOLE_1:19;

hence w <= z by YELLOW_1:3; :: thesis: verum

end;take z ; :: thesis: ( z <= x & z <= y & ( for z9 being Element of B_6 st z9 <= x & z9 <= y holds

z9 <= z ) )

( z c= x & z c= y ) by XBOOLE_1:17;

hence ( z <= x & z <= y ) by YELLOW_1:3; :: thesis: for z9 being Element of B_6 st z9 <= x & z9 <= y holds

z9 <= z

let w be Element of B_6; :: thesis: ( w <= x & w <= y implies w <= z )

assume ( w <= x & w <= y ) ; :: thesis: w <= z

then ( w c= x & w c= y ) by YELLOW_1:3;

then w c= x /\ y by XBOOLE_1:19;

hence w <= z by YELLOW_1:3; :: thesis: verum

suppose A84:
( x = 3 \ 1 & y = 3 )
; :: thesis: ex z being Element of B_6 st

( z <= x & z <= y & ( for z9 being Element of B_6 st z9 <= x & z9 <= y holds

z9 <= z ) )

( z <= x & z <= y & ( for z9 being Element of B_6 st z9 <= x & z9 <= y holds

z9 <= z ) )

(3 \ 1) /\ 3 =
(3 /\ 3) \ 1
by XBOOLE_1:49

.= 3 \ 1 ;

then reconsider z = x /\ y as Element of B_6 by A84;

take z ; :: thesis: ( z <= x & z <= y & ( for z9 being Element of B_6 st z9 <= x & z9 <= y holds

z9 <= z ) )

( z c= x & z c= y ) by XBOOLE_1:17;

hence ( z <= x & z <= y ) by YELLOW_1:3; :: thesis: for z9 being Element of B_6 st z9 <= x & z9 <= y holds

z9 <= z

let w be Element of B_6; :: thesis: ( w <= x & w <= y implies w <= z )

assume ( w <= x & w <= y ) ; :: thesis: w <= z

then ( w c= x & w c= y ) by YELLOW_1:3;

then w c= x /\ y by XBOOLE_1:19;

hence w <= z by YELLOW_1:3; :: thesis: verum

end;.= 3 \ 1 ;

then reconsider z = x /\ y as Element of B_6 by A84;

take z ; :: thesis: ( z <= x & z <= y & ( for z9 being Element of B_6 st z9 <= x & z9 <= y holds

z9 <= z ) )

( z c= x & z c= y ) by XBOOLE_1:17;

hence ( z <= x & z <= y ) by YELLOW_1:3; :: thesis: for z9 being Element of B_6 st z9 <= x & z9 <= y holds

z9 <= z

let w be Element of B_6; :: thesis: ( w <= x & w <= y implies w <= z )

assume ( w <= x & w <= y ) ; :: thesis: w <= z

then ( w c= x & w c= y ) by YELLOW_1:3;

then w c= x /\ y by XBOOLE_1:19;

hence w <= z by YELLOW_1:3; :: thesis: verum

suppose
( x = 2 & y = 0 )
; :: thesis: ex z being Element of B_6 st

( z <= x & z <= y & ( for z9 being Element of B_6 st z9 <= x & z9 <= y holds

z9 <= z ) )

then reconsider z = x /\ y as Element of B_6 ;

take z ; :: thesis: ( z <= x & z <= y & ( for z9 being Element of B_6 st z9 <= x & z9 <= y holds

z9 <= z ) )

( z c= x & z c= y ) by XBOOLE_1:17;

hence ( z <= x & z <= y ) by YELLOW_1:3; :: thesis: for z9 being Element of B_6 st z9 <= x & z9 <= y holds

z9 <= z

let w be Element of B_6; :: thesis: ( w <= x & w <= y implies w <= z )

assume ( w <= x & w <= y ) ; :: thesis: w <= z

then ( w c= x & w c= y ) by YELLOW_1:3;

then w c= x /\ y by XBOOLE_1:19;

hence w <= z by YELLOW_1:3; :: thesis: verum

end;

( z <= x & z <= y & ( for z9 being Element of B_6 st z9 <= x & z9 <= y holds

z9 <= z ) )

take z ; :: thesis: ( z <= x & z <= y & ( for z9 being Element of B_6 st z9 <= x & z9 <= y holds

z9 <= z ) )

( z c= x & z c= y ) by XBOOLE_1:17;

hence ( z <= x & z <= y ) by YELLOW_1:3; :: thesis: for z9 being Element of B_6 st z9 <= x & z9 <= y holds

z9 <= z

let w be Element of B_6; :: thesis: ( w <= x & w <= y implies w <= z )

assume ( w <= x & w <= y ) ; :: thesis: w <= z

then ( w c= x & w c= y ) by YELLOW_1:3;

then w c= x /\ y by XBOOLE_1:19;

hence w <= z by YELLOW_1:3; :: thesis: verum

suppose A85:
( x = 2 & y = 3 \ 1 )
; :: thesis: ex z being Element of B_6 st

( z <= x & z <= y & ( for z9 being Element of B_6 st z9 <= x & z9 <= y holds

z9 <= z ) )

( z <= x & z <= y & ( for z9 being Element of B_6 st z9 <= x & z9 <= y holds

z9 <= z ) )

0 in {0,1,(3 \ 1),2,(3 \ 2),3}
by ENUMSET1:def 4;

then reconsider z = 0 as Element of B_6 by YELLOW_1:1;

take z ; :: thesis: ( z <= x & z <= y & ( for z9 being Element of B_6 st z9 <= x & z9 <= y holds

z9 <= z ) )

( z c= x & z c= y ) ;

hence ( z <= x & z <= y ) by YELLOW_1:3; :: thesis: for z9 being Element of B_6 st z9 <= x & z9 <= y holds

z9 <= z

let z9 be Element of B_6; :: thesis: ( z9 <= x & z9 <= y implies z9 <= z )

assume that

A86: z9 <= x and

A87: z9 <= y ; :: thesis: z9 <= z

A88: z9 c= 3 \ 1 by A85, A87, YELLOW_1:3;

hence z9 <= z by A91, A89, A95, A93, A97, ENUMSET1:def 4; :: thesis: verum

end;then reconsider z = 0 as Element of B_6 by YELLOW_1:1;

take z ; :: thesis: ( z <= x & z <= y & ( for z9 being Element of B_6 st z9 <= x & z9 <= y holds

z9 <= z ) )

( z c= x & z c= y ) ;

hence ( z <= x & z <= y ) by YELLOW_1:3; :: thesis: for z9 being Element of B_6 st z9 <= x & z9 <= y holds

z9 <= z

let z9 be Element of B_6; :: thesis: ( z9 <= x & z9 <= y implies z9 <= z )

assume that

A86: z9 <= x and

A87: z9 <= y ; :: thesis: z9 <= z

A88: z9 c= 3 \ 1 by A85, A87, YELLOW_1:3;

A89: now :: thesis: not z9 = 2

A90:
z9 c= 2
by A85, A86, YELLOW_1:3;assume
z9 = 2
; :: thesis: contradiction

then 0 in z9 by CARD_1:50, TARSKI:def 2;

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

end;then 0 in z9 by CARD_1:50, TARSKI:def 2;

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

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

assume
z9 = 3 \ 1
; :: thesis: contradiction

then A92: 2 in z9 by TARSKI:def 2, YELLOW11:3;

not 2 in 2 ;

hence contradiction by A90, A92; :: thesis: verum

end;then A92: 2 in z9 by TARSKI:def 2, YELLOW11:3;

not 2 in 2 ;

hence contradiction by A90, A92; :: thesis: verum

A93: now :: thesis: not z9 = 3

assume
z9 = 3
; :: thesis: contradiction

then A94: 2 in z9 by CARD_1:51, ENUMSET1:def 1;

not 2 in 2 ;

hence contradiction by A90, A94; :: thesis: verum

end;then A94: 2 in z9 by CARD_1:51, ENUMSET1:def 1;

not 2 in 2 ;

hence contradiction by A90, A94; :: thesis: verum

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

assume
z9 = 3 \ 2
; :: thesis: contradiction

then A96: 2 in z9 by TARSKI:def 1, YELLOW11:4;

not 2 in 2 ;

hence contradiction by A90, A96; :: thesis: verum

end;then A96: 2 in z9 by TARSKI:def 1, YELLOW11:4;

not 2 in 2 ;

hence contradiction by A90, A96; :: thesis: verum

A97: now :: thesis: not z9 = 1

z9 is Element of {0,1,(3 \ 1),2,(3 \ 2),3}
by YELLOW_1:1;assume
z9 = 1
; :: thesis: contradiction

then 0 in z9 by CARD_1:49, TARSKI:def 1;

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

end;then 0 in z9 by CARD_1:49, TARSKI:def 1;

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

hence z9 <= z by A91, A89, A95, A93, A97, ENUMSET1:def 4; :: thesis: verum

suppose
( x = 2 & y = 2 )
; :: thesis: ex z being Element of B_6 st

( z <= x & z <= y & ( for z9 being Element of B_6 st z9 <= x & z9 <= y holds

z9 <= z ) )

then reconsider z = x /\ y as Element of B_6 ;

take z ; :: thesis: ( z <= x & z <= y & ( for z9 being Element of B_6 st z9 <= x & z9 <= y holds

z9 <= z ) )

( z c= x & z c= y ) by XBOOLE_1:17;

hence ( z <= x & z <= y ) by YELLOW_1:3; :: thesis: for z9 being Element of B_6 st z9 <= x & z9 <= y holds

z9 <= z

let w be Element of B_6; :: thesis: ( w <= x & w <= y implies w <= z )

assume ( w <= x & w <= y ) ; :: thesis: w <= z

then ( w c= x & w c= y ) by YELLOW_1:3;

then w c= x /\ y by XBOOLE_1:19;

hence w <= z by YELLOW_1:3; :: thesis: verum

end;

( z <= x & z <= y & ( for z9 being Element of B_6 st z9 <= x & z9 <= y holds

z9 <= z ) )

take z ; :: thesis: ( z <= x & z <= y & ( for z9 being Element of B_6 st z9 <= x & z9 <= y holds

z9 <= z ) )

( z c= x & z c= y ) by XBOOLE_1:17;

hence ( z <= x & z <= y ) by YELLOW_1:3; :: thesis: for z9 being Element of B_6 st z9 <= x & z9 <= y holds

z9 <= z

let w be Element of B_6; :: thesis: ( w <= x & w <= y implies w <= z )

assume ( w <= x & w <= y ) ; :: thesis: w <= z

then ( w c= x & w c= y ) by YELLOW_1:3;

then w c= x /\ y by XBOOLE_1:19;

hence w <= z by YELLOW_1:3; :: thesis: verum

suppose A98:
( x = 2 & y = 3 \ 2 )
; :: thesis: ex z being Element of B_6 st

( z <= x & z <= y & ( for z9 being Element of B_6 st z9 <= x & z9 <= y holds

z9 <= z ) )

( z <= x & z <= y & ( for z9 being Element of B_6 st z9 <= x & z9 <= y holds

z9 <= z ) )

2 misses 3 \ 2
by XBOOLE_1:79;

then 2 /\ (3 \ 2) = 0 by XBOOLE_0:def 7;

then x /\ y in {0,1,(3 \ 1),2,(3 \ 2),3} by A98, ENUMSET1:def 4;

then reconsider z = x /\ y as Element of B_6 by YELLOW_1:1;

take z ; :: thesis: ( z <= x & z <= y & ( for z9 being Element of B_6 st z9 <= x & z9 <= y holds

z9 <= z ) )

( z c= x & z c= y ) by XBOOLE_1:17;

hence ( z <= x & z <= y ) by YELLOW_1:3; :: thesis: for z9 being Element of B_6 st z9 <= x & z9 <= y holds

z9 <= z

let w be Element of B_6; :: thesis: ( w <= x & w <= y implies w <= z )

assume ( w <= x & w <= y ) ; :: thesis: w <= z

then ( w c= x & w c= y ) by YELLOW_1:3;

then w c= x /\ y by XBOOLE_1:19;

hence w <= z by YELLOW_1:3; :: thesis: verum

end;then 2 /\ (3 \ 2) = 0 by XBOOLE_0:def 7;

then x /\ y in {0,1,(3 \ 1),2,(3 \ 2),3} by A98, ENUMSET1:def 4;

then reconsider z = x /\ y as Element of B_6 by YELLOW_1:1;

take z ; :: thesis: ( z <= x & z <= y & ( for z9 being Element of B_6 st z9 <= x & z9 <= y holds

z9 <= z ) )

( z c= x & z c= y ) by XBOOLE_1:17;

hence ( z <= x & z <= y ) by YELLOW_1:3; :: thesis: for z9 being Element of B_6 st z9 <= x & z9 <= y holds

z9 <= z

let w be Element of B_6; :: thesis: ( w <= x & w <= y implies w <= z )

assume ( w <= x & w <= y ) ; :: thesis: w <= z

then ( w c= x & w c= y ) by YELLOW_1:3;

then w c= x /\ y by XBOOLE_1:19;

hence w <= z by YELLOW_1:3; :: thesis: verum

suppose A99:
( x = 2 & y = 3 )
; :: thesis: ex z being Element of B_6 st

( z <= x & z <= y & ( for z9 being Element of B_6 st z9 <= x & z9 <= y holds

z9 <= z ) )

( z <= x & z <= y & ( for z9 being Element of B_6 st z9 <= x & z9 <= y holds

z9 <= z ) )

Segm 2 c= Segm 3
by NAT_1:39;

then reconsider z = x /\ y as Element of B_6 by A99, XBOOLE_1:28;

take z ; :: thesis: ( z <= x & z <= y & ( for z9 being Element of B_6 st z9 <= x & z9 <= y holds

z9 <= z ) )

( z c= x & z c= y ) by XBOOLE_1:17;

hence ( z <= x & z <= y ) by YELLOW_1:3; :: thesis: for z9 being Element of B_6 st z9 <= x & z9 <= y holds

z9 <= z

let w be Element of B_6; :: thesis: ( w <= x & w <= y implies w <= z )

assume ( w <= x & w <= y ) ; :: thesis: w <= z

then ( w c= x & w c= y ) by YELLOW_1:3;

then w c= x /\ y by XBOOLE_1:19;

hence w <= z by YELLOW_1:3; :: thesis: verum

end;then reconsider z = x /\ y as Element of B_6 by A99, XBOOLE_1:28;

take z ; :: thesis: ( z <= x & z <= y & ( for z9 being Element of B_6 st z9 <= x & z9 <= y holds

z9 <= z ) )

( z c= x & z c= y ) by XBOOLE_1:17;

hence ( z <= x & z <= y ) by YELLOW_1:3; :: thesis: for z9 being Element of B_6 st z9 <= x & z9 <= y holds

z9 <= z

let w be Element of B_6; :: thesis: ( w <= x & w <= y implies w <= z )

assume ( w <= x & w <= y ) ; :: thesis: w <= z

then ( w c= x & w c= y ) by YELLOW_1:3;

then w c= x /\ y by XBOOLE_1:19;

hence w <= z by YELLOW_1:3; :: thesis: verum

suppose
( x = 3 \ 2 & y = 0 )
; :: thesis: ex z being Element of B_6 st

( z <= x & z <= y & ( for z9 being Element of B_6 st z9 <= x & z9 <= y holds

z9 <= z ) )

then reconsider z = x /\ y as Element of B_6 ;

take z ; :: thesis: ( z <= x & z <= y & ( for z9 being Element of B_6 st z9 <= x & z9 <= y holds

z9 <= z ) )

( z c= x & z c= y ) by XBOOLE_1:17;

hence ( z <= x & z <= y ) by YELLOW_1:3; :: thesis: for z9 being Element of B_6 st z9 <= x & z9 <= y holds

z9 <= z

let w be Element of B_6; :: thesis: ( w <= x & w <= y implies w <= z )

assume ( w <= x & w <= y ) ; :: thesis: w <= z

then ( w c= x & w c= y ) by YELLOW_1:3;

then w c= x /\ y by XBOOLE_1:19;

hence w <= z by YELLOW_1:3; :: thesis: verum

end;

( z <= x & z <= y & ( for z9 being Element of B_6 st z9 <= x & z9 <= y holds

z9 <= z ) )

take z ; :: thesis: ( z <= x & z <= y & ( for z9 being Element of B_6 st z9 <= x & z9 <= y holds

z9 <= z ) )

( z c= x & z c= y ) by XBOOLE_1:17;

hence ( z <= x & z <= y ) by YELLOW_1:3; :: thesis: for z9 being Element of B_6 st z9 <= x & z9 <= y holds

z9 <= z

let w be Element of B_6; :: thesis: ( w <= x & w <= y implies w <= z )

assume ( w <= x & w <= y ) ; :: thesis: w <= z

then ( w c= x & w c= y ) by YELLOW_1:3;

then w c= x /\ y by XBOOLE_1:19;

hence w <= z by YELLOW_1:3; :: thesis: verum

suppose
( x = 3 \ 2 & y = 3 \ 1 )
; :: thesis: ex z being Element of B_6 st

( z <= x & z <= y & ( for z9 being Element of B_6 st z9 <= x & z9 <= y holds

z9 <= z ) )

( z <= x & z <= y & ( for z9 being Element of B_6 st z9 <= x & z9 <= y holds

z9 <= z ) )

then reconsider z = x /\ y as Element of B_6 by YELLOW11:3, YELLOW11:4, ZFMISC_1:13;

take z ; :: thesis: ( z <= x & z <= y & ( for z9 being Element of B_6 st z9 <= x & z9 <= y holds

z9 <= z ) )

( z c= x & z c= y ) by XBOOLE_1:17;

hence ( z <= x & z <= y ) by YELLOW_1:3; :: thesis: for z9 being Element of B_6 st z9 <= x & z9 <= y holds

z9 <= z

let w be Element of B_6; :: thesis: ( w <= x & w <= y implies w <= z )

assume ( w <= x & w <= y ) ; :: thesis: w <= z

then ( w c= x & w c= y ) by YELLOW_1:3;

then w c= x /\ y by XBOOLE_1:19;

hence w <= z by YELLOW_1:3; :: thesis: verum

end;take z ; :: thesis: ( z <= x & z <= y & ( for z9 being Element of B_6 st z9 <= x & z9 <= y holds

z9 <= z ) )

( z c= x & z c= y ) by XBOOLE_1:17;

hence ( z <= x & z <= y ) by YELLOW_1:3; :: thesis: for z9 being Element of B_6 st z9 <= x & z9 <= y holds

z9 <= z

let w be Element of B_6; :: thesis: ( w <= x & w <= y implies w <= z )

assume ( w <= x & w <= y ) ; :: thesis: w <= z

then ( w c= x & w c= y ) by YELLOW_1:3;

then w c= x /\ y by XBOOLE_1:19;

hence w <= z by YELLOW_1:3; :: thesis: verum

suppose A100:
( x = 3 \ 2 & y = 2 )
; :: thesis: ex z being Element of B_6 st

( z <= x & z <= y & ( for z9 being Element of B_6 st z9 <= x & z9 <= y holds

z9 <= z ) )

( z <= x & z <= y & ( for z9 being Element of B_6 st z9 <= x & z9 <= y holds

z9 <= z ) )

2 misses 3 \ 2
by XBOOLE_1:79;

then 2 /\ (3 \ 2) = 0 by XBOOLE_0:def 7;

then x /\ y in {0,1,(3 \ 1),2,(3 \ 2),3} by A100, ENUMSET1:def 4;

then reconsider z = x /\ y as Element of B_6 by YELLOW_1:1;

take z ; :: thesis: ( z <= x & z <= y & ( for z9 being Element of B_6 st z9 <= x & z9 <= y holds

z9 <= z ) )

( z c= x & z c= y ) by XBOOLE_1:17;

hence ( z <= x & z <= y ) by YELLOW_1:3; :: thesis: for z9 being Element of B_6 st z9 <= x & z9 <= y holds

z9 <= z

let w be Element of B_6; :: thesis: ( w <= x & w <= y implies w <= z )

assume ( w <= x & w <= y ) ; :: thesis: w <= z

then ( w c= x & w c= y ) by YELLOW_1:3;

then w c= x /\ y by XBOOLE_1:19;

hence w <= z by YELLOW_1:3; :: thesis: verum

end;then 2 /\ (3 \ 2) = 0 by XBOOLE_0:def 7;

then x /\ y in {0,1,(3 \ 1),2,(3 \ 2),3} by A100, ENUMSET1:def 4;

then reconsider z = x /\ y as Element of B_6 by YELLOW_1:1;

take z ; :: thesis: ( z <= x & z <= y & ( for z9 being Element of B_6 st z9 <= x & z9 <= y holds

z9 <= z ) )

( z c= x & z c= y ) by XBOOLE_1:17;

hence ( z <= x & z <= y ) by YELLOW_1:3; :: thesis: for z9 being Element of B_6 st z9 <= x & z9 <= y holds

z9 <= z

let w be Element of B_6; :: thesis: ( w <= x & w <= y implies w <= z )

assume ( w <= x & w <= y ) ; :: thesis: w <= z

then ( w c= x & w c= y ) by YELLOW_1:3;

then w c= x /\ y by XBOOLE_1:19;

hence w <= z by YELLOW_1:3; :: thesis: verum

suppose
( x = 3 \ 2 & y = 3 \ 2 )
; :: thesis: ex z being Element of B_6 st

( z <= x & z <= y & ( for z9 being Element of B_6 st z9 <= x & z9 <= y holds

z9 <= z ) )

then reconsider z = x /\ y as Element of B_6 ;

take z ; :: thesis: ( z <= x & z <= y & ( for z9 being Element of B_6 st z9 <= x & z9 <= y holds

z9 <= z ) )

( z c= x & z c= y ) by XBOOLE_1:17;

hence ( z <= x & z <= y ) by YELLOW_1:3; :: thesis: for z9 being Element of B_6 st z9 <= x & z9 <= y holds

z9 <= z

let w be Element of B_6; :: thesis: ( w <= x & w <= y implies w <= z )

assume ( w <= x & w <= y ) ; :: thesis: w <= z

then ( w c= x & w c= y ) by YELLOW_1:3;

then w c= x /\ y by XBOOLE_1:19;

hence w <= z by YELLOW_1:3; :: thesis: verum

end;

( z <= x & z <= y & ( for z9 being Element of B_6 st z9 <= x & z9 <= y holds

z9 <= z ) )

take z ; :: thesis: ( z <= x & z <= y & ( for z9 being Element of B_6 st z9 <= x & z9 <= y holds

z9 <= z ) )

( z c= x & z c= y ) by XBOOLE_1:17;

hence ( z <= x & z <= y ) by YELLOW_1:3; :: thesis: for z9 being Element of B_6 st z9 <= x & z9 <= y holds

z9 <= z

let w be Element of B_6; :: thesis: ( w <= x & w <= y implies w <= z )

assume ( w <= x & w <= y ) ; :: thesis: w <= z

then ( w c= x & w c= y ) by YELLOW_1:3;

then w c= x /\ y by XBOOLE_1:19;

hence w <= z by YELLOW_1:3; :: thesis: verum

suppose A101:
( x = 3 \ 2 & y = 3 )
; :: thesis: ex z being Element of B_6 st

( z <= x & z <= y & ( for z9 being Element of B_6 st z9 <= x & z9 <= y holds

z9 <= z ) )

( z <= x & z <= y & ( for z9 being Element of B_6 st z9 <= x & z9 <= y holds

z9 <= z ) )

(3 \ 2) /\ 3 =
(3 /\ 3) \ 2
by XBOOLE_1:49

.= 3 \ 2 ;

then reconsider z = x /\ y as Element of B_6 by A101;

take z ; :: thesis: ( z <= x & z <= y & ( for z9 being Element of B_6 st z9 <= x & z9 <= y holds

z9 <= z ) )

( z c= x & z c= y ) by XBOOLE_1:17;

hence ( z <= x & z <= y ) by YELLOW_1:3; :: thesis: for z9 being Element of B_6 st z9 <= x & z9 <= y holds

z9 <= z

let w be Element of B_6; :: thesis: ( w <= x & w <= y implies w <= z )

assume ( w <= x & w <= y ) ; :: thesis: w <= z

then ( w c= x & w c= y ) by YELLOW_1:3;

then w c= x /\ y by XBOOLE_1:19;

hence w <= z by YELLOW_1:3; :: thesis: verum

end;.= 3 \ 2 ;

then reconsider z = x /\ y as Element of B_6 by A101;

take z ; :: thesis: ( z <= x & z <= y & ( for z9 being Element of B_6 st z9 <= x & z9 <= y holds

z9 <= z ) )

( z c= x & z c= y ) by XBOOLE_1:17;

hence ( z <= x & z <= y ) by YELLOW_1:3; :: thesis: for z9 being Element of B_6 st z9 <= x & z9 <= y holds

z9 <= z

let w be Element of B_6; :: thesis: ( w <= x & w <= y implies w <= z )

assume ( w <= x & w <= y ) ; :: thesis: w <= z

then ( w c= x & w c= y ) by YELLOW_1:3;

then w c= x /\ y by XBOOLE_1:19;

hence w <= z by YELLOW_1:3; :: thesis: verum

suppose
( x = 3 & y = 0 )
; :: thesis: ex z being Element of B_6 st

( z <= x & z <= y & ( for z9 being Element of B_6 st z9 <= x & z9 <= y holds

z9 <= z ) )

then reconsider z = x /\ y as Element of B_6 ;

take z ; :: thesis: ( z <= x & z <= y & ( for z9 being Element of B_6 st z9 <= x & z9 <= y holds

z9 <= z ) )

( z c= x & z c= y ) by XBOOLE_1:17;

hence ( z <= x & z <= y ) by YELLOW_1:3; :: thesis: for z9 being Element of B_6 st z9 <= x & z9 <= y holds

z9 <= z

let w be Element of B_6; :: thesis: ( w <= x & w <= y implies w <= z )

assume ( w <= x & w <= y ) ; :: thesis: w <= z

then ( w c= x & w c= y ) by YELLOW_1:3;

then w c= x /\ y by XBOOLE_1:19;

hence w <= z by YELLOW_1:3; :: thesis: verum

end;

( z <= x & z <= y & ( for z9 being Element of B_6 st z9 <= x & z9 <= y holds

z9 <= z ) )

take z ; :: thesis: ( z <= x & z <= y & ( for z9 being Element of B_6 st z9 <= x & z9 <= y holds

z9 <= z ) )

( z c= x & z c= y ) by XBOOLE_1:17;

hence ( z <= x & z <= y ) by YELLOW_1:3; :: thesis: for z9 being Element of B_6 st z9 <= x & z9 <= y holds

z9 <= z

let w be Element of B_6; :: thesis: ( w <= x & w <= y implies w <= z )

assume ( w <= x & w <= y ) ; :: thesis: w <= z

then ( w c= x & w c= y ) by YELLOW_1:3;

then w c= x /\ y by XBOOLE_1:19;

hence w <= z by YELLOW_1:3; :: thesis: verum

suppose A102:
( x = 3 & y = 3 \ 1 )
; :: thesis: ex z being Element of B_6 st

( z <= x & z <= y & ( for z9 being Element of B_6 st z9 <= x & z9 <= y holds

z9 <= z ) )

( z <= x & z <= y & ( for z9 being Element of B_6 st z9 <= x & z9 <= y holds

z9 <= z ) )

(3 \ 1) /\ 3 =
(3 /\ 3) \ 1
by XBOOLE_1:49

.= 3 \ 1 ;

then reconsider z = x /\ y as Element of B_6 by A102;

take z ; :: thesis: ( z <= x & z <= y & ( for z9 being Element of B_6 st z9 <= x & z9 <= y holds

z9 <= z ) )

( z c= x & z c= y ) by XBOOLE_1:17;

hence ( z <= x & z <= y ) by YELLOW_1:3; :: thesis: for z9 being Element of B_6 st z9 <= x & z9 <= y holds

z9 <= z

let w be Element of B_6; :: thesis: ( w <= x & w <= y implies w <= z )

assume ( w <= x & w <= y ) ; :: thesis: w <= z

then ( w c= x & w c= y ) by YELLOW_1:3;

then w c= x /\ y by XBOOLE_1:19;

hence w <= z by YELLOW_1:3; :: thesis: verum

end;.= 3 \ 1 ;

then reconsider z = x /\ y as Element of B_6 by A102;

take z ; :: thesis: ( z <= x & z <= y & ( for z9 being Element of B_6 st z9 <= x & z9 <= y holds

z9 <= z ) )

( z c= x & z c= y ) by XBOOLE_1:17;

hence ( z <= x & z <= y ) by YELLOW_1:3; :: thesis: for z9 being Element of B_6 st z9 <= x & z9 <= y holds

z9 <= z

let w be Element of B_6; :: thesis: ( w <= x & w <= y implies w <= z )

assume ( w <= x & w <= y ) ; :: thesis: w <= z

then ( w c= x & w c= y ) by YELLOW_1:3;

then w c= x /\ y by XBOOLE_1:19;

hence w <= z by YELLOW_1:3; :: thesis: verum

suppose A103:
( x = 3 & y = 2 )
; :: thesis: ex z being Element of B_6 st

( z <= x & z <= y & ( for z9 being Element of B_6 st z9 <= x & z9 <= y holds

z9 <= z ) )

( z <= x & z <= y & ( for z9 being Element of B_6 st z9 <= x & z9 <= y holds

z9 <= z ) )

Segm 2 c= Segm 3
by NAT_1:39;

then reconsider z = x /\ y as Element of B_6 by A103, XBOOLE_1:28;

take z ; :: thesis: ( z <= x & z <= y & ( for z9 being Element of B_6 st z9 <= x & z9 <= y holds

z9 <= z ) )

( z c= x & z c= y ) by XBOOLE_1:17;

hence ( z <= x & z <= y ) by YELLOW_1:3; :: thesis: for z9 being Element of B_6 st z9 <= x & z9 <= y holds

z9 <= z

let w be Element of B_6; :: thesis: ( w <= x & w <= y implies w <= z )

assume ( w <= x & w <= y ) ; :: thesis: w <= z

then ( w c= x & w c= y ) by YELLOW_1:3;

then w c= x /\ y by XBOOLE_1:19;

hence w <= z by YELLOW_1:3; :: thesis: verum

end;then reconsider z = x /\ y as Element of B_6 by A103, XBOOLE_1:28;

take z ; :: thesis: ( z <= x & z <= y & ( for z9 being Element of B_6 st z9 <= x & z9 <= y holds

z9 <= z ) )

( z c= x & z c= y ) by XBOOLE_1:17;

hence ( z <= x & z <= y ) by YELLOW_1:3; :: thesis: for z9 being Element of B_6 st z9 <= x & z9 <= y holds

z9 <= z

let w be Element of B_6; :: thesis: ( w <= x & w <= y implies w <= z )

assume ( w <= x & w <= y ) ; :: thesis: w <= z

then ( w c= x & w c= y ) by YELLOW_1:3;

then w c= x /\ y by XBOOLE_1:19;

hence w <= z by YELLOW_1:3; :: thesis: verum

suppose A104:
( x = 3 & y = 3 \ 2 )
; :: thesis: ex z being Element of B_6 st

( z <= x & z <= y & ( for z9 being Element of B_6 st z9 <= x & z9 <= y holds

z9 <= z ) )

( z <= x & z <= y & ( for z9 being Element of B_6 st z9 <= x & z9 <= y holds

z9 <= z ) )

(3 \ 2) /\ 3 =
(3 /\ 3) \ 2
by XBOOLE_1:49

.= 3 \ 2 ;

then reconsider z = x /\ y as Element of B_6 by A104;

take z ; :: thesis: ( z <= x & z <= y & ( for z9 being Element of B_6 st z9 <= x & z9 <= y holds

z9 <= z ) )

( z c= x & z c= y ) by XBOOLE_1:17;

hence ( z <= x & z <= y ) by YELLOW_1:3; :: thesis: for z9 being Element of B_6 st z9 <= x & z9 <= y holds

z9 <= z

let w be Element of B_6; :: thesis: ( w <= x & w <= y implies w <= z )

assume ( w <= x & w <= y ) ; :: thesis: w <= z

then ( w c= x & w c= y ) by YELLOW_1:3;

then w c= x /\ y by XBOOLE_1:19;

hence w <= z by YELLOW_1:3; :: thesis: verum

end;.= 3 \ 2 ;

then reconsider z = x /\ y as Element of B_6 by A104;

take z ; :: thesis: ( z <= x & z <= y & ( for z9 being Element of B_6 st z9 <= x & z9 <= y holds

z9 <= z ) )

( z c= x & z c= y ) by XBOOLE_1:17;

hence ( z <= x & z <= y ) by YELLOW_1:3; :: thesis: for z9 being Element of B_6 st z9 <= x & z9 <= y holds

z9 <= z

let w be Element of B_6; :: thesis: ( w <= x & w <= y implies w <= z )

assume ( w <= x & w <= y ) ; :: thesis: w <= z

then ( w c= x & w c= y ) by YELLOW_1:3;

then w c= x /\ y by XBOOLE_1:19;

hence w <= z by YELLOW_1:3; :: thesis: verum

suppose
( x = 3 & y = 3 )
; :: thesis: ex z being Element of B_6 st

( z <= x & z <= y & ( for z9 being Element of B_6 st z9 <= x & z9 <= y holds

z9 <= z ) )

then reconsider z = x /\ y as Element of B_6 ;

take z ; :: thesis: ( z <= x & z <= y & ( for z9 being Element of B_6 st z9 <= x & z9 <= y holds

z9 <= z ) )

( z c= x & z c= y ) by XBOOLE_1:17;

hence ( z <= x & z <= y ) by YELLOW_1:3; :: thesis: for z9 being Element of B_6 st z9 <= x & z9 <= y holds

z9 <= z

let w be Element of B_6; :: thesis: ( w <= x & w <= y implies w <= z )

assume ( w <= x & w <= y ) ; :: thesis: w <= z

then ( w c= x & w c= y ) by YELLOW_1:3;

then w c= x /\ y by XBOOLE_1:19;

hence w <= z by YELLOW_1:3; :: thesis: verum

end;

( z <= x & z <= y & ( for z9 being Element of B_6 st z9 <= x & z9 <= y holds

z9 <= z ) )

take z ; :: thesis: ( z <= x & z <= y & ( for z9 being Element of B_6 st z9 <= x & z9 <= y holds

z9 <= z ) )

( z c= x & z c= y ) by XBOOLE_1:17;

hence ( z <= x & z <= y ) by YELLOW_1:3; :: thesis: for z9 being Element of B_6 st z9 <= x & z9 <= y holds

z9 <= z

let w be Element of B_6; :: thesis: ( w <= x & w <= y implies w <= z )

assume ( w <= x & w <= y ) ; :: thesis: w <= z

then ( w c= x & w c= y ) by YELLOW_1:3;

then w c= x /\ y by XBOOLE_1:19;

hence w <= z by YELLOW_1:3; :: thesis: verum