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