let X be non empty 1-sorted ; :: thesis: for A1, A2 being Subset of X st ( A1 = A2 ` or A2 = A1 ` ) holds

A1,A2 constitute_a_decomposition

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

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

then ( A1 misses A2 & A1 \/ A2 = [#] X ) by SUBSET_1:23, TDLAT_1:1;

hence A1,A2 constitute_a_decomposition ; :: thesis: verum

A1,A2 constitute_a_decomposition

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

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

then ( A1 misses A2 & A1 \/ A2 = [#] X ) by SUBSET_1:23, TDLAT_1:1;

hence A1,A2 constitute_a_decomposition ; :: thesis: verum