id the carrier of S1, id the carrier' of S1 form_morphism_between S1,S2 by Def2;
hence A | S1 is non-empty by Th23; :: thesis: verum