for L being LATTICE
for a, b being Element of L st L is modular holds
subrelstr [#b,(a "\/" b)#], subrelstr [#(a "/\" b),a#] are_isomorphic