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 )

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

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

given X being non empty Ring_of_sets such that A3:
L, InclPoset X are_isomorphic
; :: thesis: L is distributive
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;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

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