let X be non empty TopSpace; :: 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 by Def1;
then A3: A1 c= A2 ` by TDLAT_1:2;
A4: A2 c= A1 ` by A2, TDLAT_1:2;
A5: A1 \/ A2 = [#] X by A1, Def1;
then A2 ` c= A1 by TDLAT_1:1;
hence A1 = A2 ` by A3, XBOOLE_0:def 10; :: thesis: A2 = A1 `
A1 ` c= A2 by A5, TDLAT_1:1;
hence A2 = A1 ` by A4, XBOOLE_0:def 10; :: thesis: verum