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

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