let X be non empty 1-sorted ; :: thesis: for A, A1, A2 being Subset of X st A1,A constitute_a_decomposition & A,A2 constitute_a_decomposition holds

A1 = A2

let A, A1, A2 be Subset of X; :: thesis: ( A1,A constitute_a_decomposition & A,A2 constitute_a_decomposition implies A1 = A2 )

assume A1,A constitute_a_decomposition ; :: thesis: ( not A,A2 constitute_a_decomposition or A1 = A2 )

then A1: A1 = A ` by Th3;

assume A,A2 constitute_a_decomposition ; :: thesis: A1 = A2

hence A1 = A2 by A1, Th3; :: thesis: verum

A1 = A2

let A, A1, A2 be Subset of X; :: thesis: ( A1,A constitute_a_decomposition & A,A2 constitute_a_decomposition implies A1 = A2 )

assume A1,A constitute_a_decomposition ; :: thesis: ( not A,A2 constitute_a_decomposition or A1 = A2 )

then A1: A1 = A ` by Th3;

assume A,A2 constitute_a_decomposition ; :: thesis: A1 = A2

hence A1 = A2 by A1, Th3; :: thesis: verum