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

assume A1: L is distributive ; :: thesis: ex X being non empty Ring_of_sets st L, InclPoset X are_isomorphic
consider X being set such that
A2: X = LOWER (subrelstr (Join-IRR L)) ;
A3: X is Ring_of_sets by A2, Th15;
L, InclPoset X are_isomorphic by A1, A2, Th14;
hence ex X being non empty Ring_of_sets st L, InclPoset X are_isomorphic by A2, A3; :: thesis: verum

end;

given X being non empty Ring_of_sets such that A4: L, InclPoset X are_isomorphic ; :: thesis: L is distributive
consider f being Function of L,(InclPoset X) such that
A5: f is isomorphic by A4, WAYBEL_1:def 8;
A6: f is infs-preserving by A5, WAYBEL13:20;
f is sups-preserving by A5, WAYBEL13:20;
then A7: f is join-preserving by Lm3;
f is one-to-one by A5, WAYBEL_0:66;
hence L is distributive by A6, A7, Lm2, WAYBEL_6:3; :: thesis: verum