let L1, L2 be lower-bounded LATTICE; :: thesis: ( L1,L2 are_isomorphic & L1 is modular implies L2 is modular )
assume A1: ( L1,L2 are_isomorphic & L1 is modular ) ; :: thesis: L2 is modular
then consider f being Function of L1,L2 such that
A2: f is isomorphic by WAYBEL_1:def 8;
( f is infs-preserving & f is sups-preserving ) by A2, WAYBEL13:20;
then A3: ( f is meet-preserving & f is join-preserving ) by Th4;
let a, b, c be Element of L2; :: according to YELLOW11:def 3 :: thesis: ( not a <= c or a "\/" (b "/\" c) = (a "\/" b) "/\" c )
assume A4: a <= c ; :: thesis: a "\/" (b "/\" c) = (a "\/" b) "/\" c
set A = (f " ) . a;
set B = (f " ) . b;
set C = (f " ) . c;
A5: ( f is one-to-one & rng f = the carrier of L2 ) by A2, WAYBEL_0:66;
then A6: ( f is one-to-one & a in rng f & b in rng f & c in rng f & a = f . ((f " ) . a) & b = f . ((f " ) . b) & c = f . ((f " ) . c) ) by FUNCT_1:57;
( (f " ) . a in dom f & (f " ) . b in dom f & (f " ) . c in dom f ) by A5, FUNCT_1:54;
then reconsider A = (f " ) . a, B = (f " ) . b, C = (f " ) . c as Element of L1 ;
A <= C by A2, A4, A6, WAYBEL_0:66;
then A7: A "\/" (B "/\" C) = (A "\/" B) "/\" C by A1, YELLOW11:def 3;
thus a "\/" (b "/\" c) = (f . A) "\/" (f . (B "/\" C)) by A3, A6, WAYBEL_6:1
.= f . ((A "\/" B) "/\" C) by A3, A7, WAYBEL_6:2
.= (f . (A "\/" B)) "/\" (f . C) by A3, WAYBEL_6:1
.= (a "\/" b) "/\" c by A3, A6, WAYBEL_6:2 ; :: thesis: verum