let S, T be LATTICE; :: thesis: for f being Function of S,T st T is distributive & f is meet-preserving & f is join-preserving & f is one-to-one holds
S is distributive
let f be Function of S,T; :: thesis: ( T is distributive & f is meet-preserving & f is join-preserving & f is one-to-one implies S is distributive )
assume that
A1: T is distributive and
A2: ( f is meet-preserving & f is join-preserving & f is one-to-one ) ; :: thesis: S is distributive
let x, y, z be Element of S; :: according to WAYBEL_1:def 3 :: thesis: 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; :: thesis: verum