let X be non empty 1-sorted ; :: thesis: for A1, A2 being Subset of X st A1,A2 constitute_a_decomposition holds
( A1 = A2 ` & A2 = A1 ` )
let A1, A2 be Subset of X; :: thesis: ( A1,A2 constitute_a_decomposition implies ( A1 = A2 ` & A2 = A1 ` ) )
assume A1: A1,A2 constitute_a_decomposition ; :: thesis: ( A1 = A2 ` & A2 = A1 ` )
then A2: A1 misses A2 ;
then A3: A1 c= A2 ` by SUBSET_1:23;
A4: A2 c= A1 ` by A2, SUBSET_1:23;
A5: A1 \/ A2 = [#] X by A1;
then A2 ` c= A1 by TDLAT_1:1;
hence A1 = A2 ` by A3; :: thesis: A2 = A1 `
A1 ` c= A2 by A5, TDLAT_1:1;
hence A2 = A1 ` by A4; :: thesis: verum