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 one-to-one & 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 ) by Def3;
A2: Image f is modular by A1, Th8;
A3: ( Image f is lower-bounded LATTICE & corestr f is one-to-one ) by A1, Th6, WAYBEL_1:32;
A4: rng (corestr f) = the carrier of (Image f) by FUNCT_2:def 3;
A5: for x, y being Element of L st x <= y holds
(corestr f) . x <= (corestr f) . y by WAYBEL_1:def 2;
for x, y being Element of L st (corestr f) . x <= (corestr f) . y holds
x <= y by A1, Th7;
then corestr f is isomorphic by A3, A4, A5, WAYBEL_0:66;
then L, Image f are_isomorphic by WAYBEL_1:def 8;
hence L is modular by A2, A3, Th5, WAYBEL_1:7; :: thesis: verum