-theorem lsubf_sor: āK,L,g1,f1. ā¦K, g1ā¦ ā«š
* ā¦L, f1ā¦ ā
- āg2,f2. ā¦K, g2ā¦ ā«š
* ā¦L, f2ā¦ ā
- āg. g1 ā g2 ā g ā āf. f1 ā f2 ā f ā ā¦K, gā¦ ā«š
* ā¦L, fā¦.
+theorem lsubf_sor:
+ āK,L,g1,f1. āØK,g1ā© ā«š
+ āØL,f1ā© ā
+ āg2,f2. āØK,g2ā© ā«š
+ āØL,f2ā© ā
+ āg. g1 ā g2 ā g ā āf. f1 ā f2 ā f ā āØK,gā© ā«š
+ āØL,fā©.