Loading [MathJax]/extensions/tex2jax.js
Lm1:
for A, B, C being set st C c= B holds
A \ C = (A \ B) \/ (A /\ (B \ C))
Lm2:
for X being set
for A1 being SetSequence of X st A1 is non-descending holds
for n being Nat holds (Partial_Union A1) . n = A1 . n