theorem Th20: :: FLANG_1:20

for E being set
for A, B, C being Subset of (E ^omega) holds
( (A ^^ B) \/ (A ^^ C) = A ^^ (B \/ C) & (B ^^ A) \/ (C ^^ A) = (B \/ C) ^^ A )