consider S9 being non void strict Signature;

per cases ( S is empty or not S is empty ) ;

suppose S is empty ; :: thesis: ex b₁ being Extension of S st
( not b₁ is empty & not b₁ is void & b₁ is strict )

then S9 is Extension of S by Th53;
hence ex b₁ being Extension of S st
( not b₁ is empty & not b₁ is void & b₁ is strict ) ; :: thesis: verum

end;

suppose not S is empty ; :: thesis: ex b₁ being Extension of S st
( not b₁ is empty & not b₁ is void & b₁ is strict )

then reconsider S1 = S as non empty Signature ;
consider s being SortSymbol of S9, o being OperSymbol of S9;
reconsider E = S9 +* S1 as Extension of S by Th50;
take E ; :: thesis: ( not E is empty & not E is void & E is strict )
thus not the carrier of E is empty ; :: according to STRUCT_0:def 1 :: thesis: ( not E is void & E is strict )
thus not the carrier' of E is empty ; :: according to STRUCT_0:def 13 :: thesis: E is strict
thus E is strict ; :: thesis: verum

end;

end;