theorem Th3: :: LATTICE5:3

for A being non empty set st A is c=-linear holds
[:(union A),(union A):] = union { [:a,a:] where a is Element of A : a in A }