let L be finite LATTICE; :: thesis: ( L is distributive iff ex X being non empty Ring_of_sets st L, InclPoset X are_isomorphic )
thus ( L is distributive implies ex X being non empty Ring_of_sets st L, InclPoset X are_isomorphic ) :: thesis: ( ex X being non empty Ring_of_sets st L, InclPoset X are_isomorphic implies L is distributive )
proof
consider X being set such that
A1: X = LOWER (subrelstr (Join-IRR L)) ;
A2: X is Ring_of_sets by A1, Th15;
assume L is distributive ; :: thesis: ex X being non empty Ring_of_sets st L, InclPoset X are_isomorphic
then L, InclPoset X are_isomorphic by A1, Th14;
hence ex X being non empty Ring_of_sets st L, InclPoset X are_isomorphic by A1, A2; :: thesis: verum
end;
given X being non empty Ring_of_sets such that A3: L, InclPoset X are_isomorphic ; :: thesis: L is distributive
consider f being Function of L,(InclPoset X) such that
A4: f is isomorphic by A3;
A5: f is V13() by A4, WAYBEL_0:66;
( f is infs-preserving & f is join-preserving ) by A4, Lm3, WAYBEL13:20;
hence L is distributive by A5, Lm2, WAYBEL_6:3; :: thesis: verum