let C be Chain; :: thesis: C is distributive

for x, y, z being Element of C holds x "/\" (y "\/" z) = (x "/\" y) "\/" (x "/\" z)

for x, y, z being Element of C holds x "/\" (y "\/" z) = (x "/\" y) "\/" (x "/\" z)

proof

hence
C is distributive
; :: thesis: verum
let x, y, z be Element of C; :: thesis: x "/\" (y "\/" z) = (x "/\" y) "\/" (x "/\" z)

A1: x <= x ;

end;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;

end;

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;.= 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

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;.= 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

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;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

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;.= 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

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;.= 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

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;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

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;.= 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

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;.= 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