let S, T be LATTICE; for f being Function of S,T st T is distributive & f is meet-preserving & f is join-preserving & f is V27() holds
S is distributive
let f be Function of S,T; ( T is distributive & f is meet-preserving & f is join-preserving & f is V27() implies S is distributive )
assume that
A1:
T is distributive
and
A2:
( f is meet-preserving & f is join-preserving & f is V27() )
; S is distributive
let x, y, z be Element of S; WAYBEL_1:def 3 x "/\" (y "\/" z) = (x "/\" y) "\/" (x "/\" z)
f . (x "/\" (y "\/" z)) =
(f . x) "/\" (f . (y "\/" z))
by A2, Th1
.=
(f . x) "/\" ((f . y) "\/" (f . z))
by A2, Th2
.=
((f . x) "/\" (f . y)) "\/" ((f . x) "/\" (f . z))
by A1
.=
((f . x) "/\" (f . y)) "\/" (f . (x "/\" z))
by A2, Th1
.=
(f . (x "/\" y)) "\/" (f . (x "/\" z))
by A2, Th1
.=
f . ((x "/\" y) "\/" (x "/\" z))
by A2, Th2
;
hence
x "/\" (y "\/" z) = (x "/\" y) "\/" (x "/\" z)
by A2; verum