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;

then A4: A1 = A2 by A1, A3;

UAp A = B1 by A2;

then B1 = B2 by A1, A3;

hence A = B by A2, A4, A3; :: thesis: verum

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;

then A4: A1 = A2 by A1, A3;

UAp A = B1 by A2;

then B1 = B2 by A1, A3;

hence A = B by A2, A4, A3; :: thesis: verum