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