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