set I = the carrier of S;
set Y = X (\/) ( the carrier of S --> );
set R = Reverse (X (\/) ( the carrier of S --> ));
(Reverse (X (\/) ( the carrier of S --> ))) "" X is ManySortedSubset of FreeGen (X (\/) ( the carrier of S --> )) by EQUATION:8;
then A1: (Reverse (X (\/) ( the carrier of S --> ))) "" X c= FreeGen (X (\/) ( the carrier of S --> )) by PBOOLE:def 18;
FreeGen (X (\/) ( the carrier of S --> )) c= the Sorts of (FreeMSA (X (\/) ( the carrier of S --> ))) by PBOOLE:def 18;
then (Reverse (X (\/) ( the carrier of S --> ))) "" X c= the Sorts of (FreeMSA (X (\/) ( the carrier of S --> ))) by ;
then reconsider Z = (Reverse (X (\/) ( the carrier of S --> ))) "" X as MSSubset of (FreeMSA (X (\/) ( the carrier of S --> ))) by PBOOLE:def 18;
take GenMSAlg Z ; :: thesis: ex A being MSSubset of (FreeMSA (X (\/) ( the carrier of S --> ))) st
( GenMSAlg Z = GenMSAlg A & A = (Reverse (X (\/) ( the carrier of S --> ))) "" X )

take Z ; :: thesis: ( GenMSAlg Z = GenMSAlg Z & Z = (Reverse (X (\/) ( the carrier of S --> ))) "" X )
thus ( GenMSAlg Z = GenMSAlg Z & Z = (Reverse (X (\/) ( the carrier of S --> ))) "" X ) ; :: thesis: verum