Josh needs a property for which there is an obvious pointwise proof. He wonders whether it is possible to prove it in point-free style. I haven’t practised point-free proofs for a while, so I’d give it a try.

The actual property he needs is that

$S\; \subseteq \; C\; .\; S\; \Leftarrow \; R\; \subseteq \; C\; .\; R\; \wedge \; S\; \subseteq \; R$

Intuitively speaking, if

Well, the proof goes:

$C\; .\; S$

={ since C . C = C }

C . C . S

⊇{ since X ⊇ X ∩ Y }

C . ((C . S) ∩ R)

⊇{ modular law X ∩ (Y.Z) ⊆ Y . ((Y˘.X) ∩ Z) , andC˘ = C }

S ∩ (C . R)

⊇{ given: R ⊆ C . R }

S ∩ R

={ given: S ⊆ R }

S

It is hard to explain the intuition behind the use of modular law. If we take

$(b\; S\; a\; \Rightarrow \; C\; b\; \wedge \; b\; S\; a)\; \Leftarrow \; (b\; R\; a\; \Rightarrow \; C\; b\; \wedge \; b\; R\; a)\; \wedge \; b\; S\; a\; \Rightarrow \; b\; R\; a$

where

$C\; b\; \wedge \; b\; S\; a$

⇐{ strengthening }

C b ∧ b S a ∧ b R a

⇐{ since b R a ⇒ C b ∧ b R a }

b S a ∧ b R a

⇐{ since b S a ⇒ b R a }

b S a

The strengthening step corresponds to the use of