for X being set
for A, B being Subset of X holds Complement (A followed_by B) = (A `) followed_by (B `) by Lm1;