let L be lower-bounded LATTICE; :: thesis: ( L has_a_representation_of_type<= 2 implies L is modular )
assume L has_a_representation_of_type<= 2 ; :: thesis: L is modular
then consider A being non trivial set , f being Homomorphism of L,(EqRelLATT A) such that
A1: f is V17() and
A2: ( Image f is finitely_typed & ex e being Equivalence_Relation of A st
( e in the carrier of (Image f) & e <> id A ) & type_of (Image f) <= 2 ) ;
A3: ( rng (corestr f) = the carrier of (Image f) & ( for x, y being Element of L st x <= y holds
(corestr f) . x <= (corestr f) . y ) ) by FUNCT_2:def 3, WAYBEL_1:def 2;
( corestr f is V17() & ( for x, y being Element of L st (corestr f) . x <= (corestr f) . y holds
x <= y ) ) by A1, Th7, WAYBEL_1:30;
then corestr f is isomorphic by A3, WAYBEL_0:66;
then A4: L, Image f are_isomorphic by WAYBEL_1:def 8;
A5: Image f is lower-bounded LATTICE by Th6;
Image f is modular by A2, Th8;
hence L is modular by A5, A4, Th5, WAYBEL_1:6; :: thesis: verum