set S9 = the non void strict Signature;
per cases ( S is empty or not S is empty ) ;
suppose S is empty ; :: thesis: ex b1 being Extension of S st
( not b1 is empty & not b1 is void & b1 is strict )
then the non void strict Signature is Extension of S by Th51;
hence ex b1 being Extension of S st
( not b1 is empty & not b1 is void & b1 is strict ) ; :: thesis: verum
end;
suppose not S is empty ; :: thesis: ex b1 being Extension of S st
( not b1 is empty & not b1 is void & b1 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;