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 V27() 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 V27() implies S is distributive )

assume that

A1: T is distributive and

A2: ( f is meet-preserving & f is join-preserving & f is V27() ) ; :: 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

S is distributive

let f be Function of S,T; :: thesis: ( 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() ) ; :: 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