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 ;
(x "/\" y) "\/" (x "/\" z) = x "\/" (x "/\" z) by
.= x "\/" x by
.= x by ;
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 ;
(x "/\" y) "\/" (x "/\" z) = x "\/" (x "/\" z) by
.= x "\/" x by
.= x by ;
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 ;
A8: x "/\" (y "\/" z) = x "/\" z by
.= z by ;
(x "/\" y) "\/" (x "/\" z) = x "\/" (x "/\" z) by
.= x "\/" z by
.= x by ;
hence x "/\" (y "\/" z) = (x "/\" y) "\/" (x "/\" z) by ; :: 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 ;
(x "/\" y) "\/" (x "/\" z) = x "\/" (x "/\" z) by
.= x "\/" z by
.= x by ;
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 ;
(x "/\" y) "\/" (x "/\" z) = y "\/" (x "/\" z) by
.= y "\/" x by
.= x by ;
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 ;
A15: x "/\" (y "\/" z) = x "/\" y by
.= y by ;
(x "/\" y) "\/" (x "/\" z) = y "\/" (x "/\" z) by
.= y "\/" x by
.= x by ;
hence x "/\" (y "\/" z) = (x "/\" y) "\/" (x "/\" z) by ; :: 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 ;
(x "/\" y) "\/" (x "/\" z) = y "\/" (x "/\" z) by
.= y "\/" z by
.= z by ;
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 ;
(x "/\" y) "\/" (x "/\" z) = y "\/" (x "/\" z) by
.= y "\/" z by
.= y by ;
hence x "/\" (y "\/" z) = (x "/\" y) "\/" (x "/\" z) by A19; :: thesis: verum
end;
end;
end;
hence C is distributive ; :: thesis: verum