thus ( A = B implies ( LAp A = LAp B & UAp A = UAp B ) ) ; :: thesis: ( LAp A = LAp B & UAp A = UAp B implies A = B )
assume A1: ( LAp A = LAp B & UAp A = UAp B ) ; :: thesis: A = B
consider A1, B1 being Subset of X such that
A2: A = [A1,B1] by Th55;
consider A2, B2 being Subset of X such that
A3: B = [A2,B2] by Th55;
LAp A = A1 by A2, MCART_1:7;
then A4: A1 = A2 by A1, A3, MCART_1:7;
UAp A = B1 by A2, MCART_1:7;
hence A = B by A2, A4, A3, A1, MCART_1:7; :: thesis: verum