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

( 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