= minus_star_image o2 o3 b' (A o2 (minus_star_image o1 o2 a' (A o1 X))));
[2: intro; apply sym1; apply (.= #‡(†((H' ?)\sup -1))); apply sym1; apply (K X);]
clear K H' H1';
= minus_star_image o2 o3 b' (A o2 (minus_star_image o1 o2 a' (A o1 X))));
[2: intro; apply sym1; apply (.= #‡(†((H' ?)\sup -1))); apply sym1; apply (K X);]
clear K H' H1';