set S9 = the 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 the non void strict Signature is Extension of S by Th51;
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 ;
reconsider E = the non void strict Signature +* S1 as Extension of S by Th48;
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;