theorem :: ALGSPEC1:50

for S1, S2, E being non empty Signature holds
( E is Extension of S1 & E is Extension of S2 iff ( S1 tolerates S2 & E is Extension of S1 +* S2 ) )