let C be Chain; :: thesis: C is distributive
for x, y, z being Element of C holds x "/\" (y "\/" z) = (x "/\" y) "\/" (x "/\" z)

proof

let x, y, z be Element of C; :: thesis: x "/\" (y "\/" z) = (x "/\" y) "\/" (x "/\" z)
A1: x <= x ;

per cases ( ( x <= y & x <= z & y <= z ) or ( x <= y & x <= z & y >= z ) or ( x <= y & x >= z & y <= z ) or ( x <= y & x >= z & y >= z ) or ( x >= y & x <= z & y <= z ) or ( x >= y & x <= z & y >= z ) or ( x >= y & x >= z & y <= z ) or ( x >= y & x >= z & y >= z ) ) by WAYBEL_0:def 29;

suppose A2: ( x <= y & x <= z & y <= z ) ; :: thesis: x "/\" (y "\/" z) = (x "/\" y) "\/" (x "/\" z)

then A3: x "/\" (y "\/" z) = x "/\" z by YELLOW_0:24
.= x by A2, YELLOW_0:25 ;
(x "/\" y) "\/" (x "/\" z) = x "\/" (x "/\" z) by A2, YELLOW_0:25
.= x "\/" x by A2, YELLOW_0:25
.= x by A1, YELLOW_0:24 ;
hence x "/\" (y "\/" z) = (x "/\" y) "\/" (x "/\" z) by A3; :: thesis: verum

end;

suppose A4: ( x <= y & x <= z & y >= z ) ; :: thesis: x "/\" (y "\/" z) = (x "/\" y) "\/" (x "/\" z)

then A5: x "/\" (y "\/" z) = x "/\" y by YELLOW_0:24
.= x by A4, YELLOW_0:25 ;
(x "/\" y) "\/" (x "/\" z) = x "\/" (x "/\" z) by A4, YELLOW_0:25
.= x "\/" x by A4, YELLOW_0:25
.= x by A1, YELLOW_0:24 ;
hence x "/\" (y "\/" z) = (x "/\" y) "\/" (x "/\" z) by A5; :: thesis: verum

end;

suppose A6: ( x <= y & x >= z & y <= z ) ; :: thesis: x "/\" (y "\/" z) = (x "/\" y) "\/" (x "/\" z)

then z <= y by YELLOW_0:def 2;
then A7: z = y by A6, YELLOW_0:def 3;
A8: x "/\" (y "\/" z) = x "/\" z by A6, YELLOW_0:24
.= z by A6, YELLOW_0:25 ;
(x "/\" y) "\/" (x "/\" z) = x "\/" (x "/\" z) by A6, YELLOW_0:25
.= x "\/" z by A6, YELLOW_0:25
.= x by A6, YELLOW_0:24 ;
hence x "/\" (y "\/" z) = (x "/\" y) "\/" (x "/\" z) by A6, A7, A8, YELLOW_0:def 3; :: thesis: verum

end;

suppose A9: ( x <= y & x >= z & y >= z ) ; :: thesis: x "/\" (y "\/" z) = (x "/\" y) "\/" (x "/\" z)

then A10: x "/\" (y "\/" z) = x "/\" y by YELLOW_0:24
.= x by A9, YELLOW_0:25 ;
(x "/\" y) "\/" (x "/\" z) = x "\/" (x "/\" z) by A9, YELLOW_0:25
.= x "\/" z by A9, YELLOW_0:25
.= x by A9, YELLOW_0:24 ;
hence x "/\" (y "\/" z) = (x "/\" y) "\/" (x "/\" z) by A10; :: thesis: verum

end;

suppose A11: ( x >= y & x <= z & y <= z ) ; :: thesis: x "/\" (y "\/" z) = (x "/\" y) "\/" (x "/\" z)

then A12: x "/\" (y "\/" z) = x "/\" z by YELLOW_0:24
.= x by A11, YELLOW_0:25 ;
(x "/\" y) "\/" (x "/\" z) = y "\/" (x "/\" z) by A11, YELLOW_0:25
.= y "\/" x by A11, YELLOW_0:25
.= x by A11, YELLOW_0:24 ;
hence x "/\" (y "\/" z) = (x "/\" y) "\/" (x "/\" z) by A12; :: thesis: verum

end;

suppose A13: ( x >= y & x <= z & y >= z ) ; :: thesis: x "/\" (y "\/" z) = (x "/\" y) "\/" (x "/\" z)

then z >= y by YELLOW_0:def 2;
then A14: z = y by A13, YELLOW_0:def 3;
A15: x "/\" (y "\/" z) = x "/\" y by A13, YELLOW_0:24
.= y by A13, YELLOW_0:25 ;
(x "/\" y) "\/" (x "/\" z) = y "\/" (x "/\" z) by A13, YELLOW_0:25
.= y "\/" x by A13, YELLOW_0:25
.= x by A13, YELLOW_0:24 ;
hence x "/\" (y "\/" z) = (x "/\" y) "\/" (x "/\" z) by A13, A14, A15, YELLOW_0:def 3; :: thesis: verum

end;

suppose A16: ( x >= y & x >= z & y <= z ) ; :: thesis: x "/\" (y "\/" z) = (x "/\" y) "\/" (x "/\" z)

then A17: x "/\" (y "\/" z) = x "/\" z by YELLOW_0:24
.= z by A16, YELLOW_0:25 ;
(x "/\" y) "\/" (x "/\" z) = y "\/" (x "/\" z) by A16, YELLOW_0:25
.= y "\/" z by A16, YELLOW_0:25
.= z by A16, YELLOW_0:24 ;
hence x "/\" (y "\/" z) = (x "/\" y) "\/" (x "/\" z) by A17; :: thesis: verum

end;

suppose A18: ( x >= y & x >= z & y >= z ) ; :: thesis: x "/\" (y "\/" z) = (x "/\" y) "\/" (x "/\" z)

then A19: x "/\" (y "\/" z) = x "/\" y by YELLOW_0:24
.= y by A18, YELLOW_0:25 ;
(x "/\" y) "\/" (x "/\" z) = y "\/" (x "/\" z) by A18, YELLOW_0:25
.= y "\/" z by A18, YELLOW_0:25
.= y by A18, YELLOW_0:24 ;
hence x "/\" (y "\/" z) = (x "/\" y) "\/" (x "/\" z) by A19; :: thesis: verum

end;

end;

end;

hence C is distributive ; :: thesis: verum