let X be non empty 1-sorted ; for A1, A2, B1, B2 being Subset of X st A1,A2 constitute_a_decomposition & B1,B2 constitute_a_decomposition holds
A1 /\ B1,A2 \/ B2 constitute_a_decomposition
let A1, A2, B1, B2 be Subset of X; ( A1,A2 constitute_a_decomposition & B1,B2 constitute_a_decomposition implies A1 /\ B1,A2 \/ B2 constitute_a_decomposition )
assume A1:
A1,A2 constitute_a_decomposition
; ( not B1,B2 constitute_a_decomposition or A1 /\ B1,A2 \/ B2 constitute_a_decomposition )
then
A1 misses A2
;
then A2:
A1 /\ A2 = {}
;
assume A3:
B1,B2 constitute_a_decomposition
; A1 /\ B1,A2 \/ B2 constitute_a_decomposition
then A4:
B1 \/ B2 = [#] X
;
B1 misses B2
by A3;
then A5:
B1 /\ B2 = {} X
;
(A1 /\ B1) /\ (A2 \/ B2) =
((B1 /\ A1) /\ A2) \/ ((A1 /\ B1) /\ B2)
by XBOOLE_1:23
.=
(B1 /\ (A1 /\ A2)) \/ ((A1 /\ B1) /\ B2)
by XBOOLE_1:16
.=
(B1 /\ (A1 /\ A2)) \/ (A1 /\ (B1 /\ B2))
by XBOOLE_1:16
.=
{} X
by A5, A2
;
then A6:
A1 /\ B1 misses A2 \/ B2
;
(A1 /\ B1) \/ (A2 \/ B2) =
(A1 \/ (A2 \/ B2)) /\ (B1 \/ (A2 \/ B2))
by XBOOLE_1:24
.=
((A1 \/ A2) \/ B2) /\ (B1 \/ (B2 \/ A2))
by XBOOLE_1:4
.=
((A1 \/ A2) \/ B2) /\ ((B1 \/ B2) \/ A2)
by XBOOLE_1:4
.=
(([#] X) \/ B2) /\ (([#] X) \/ A2)
by A1, A4
.=
(([#] X) \/ B2) /\ ([#] X)
by XBOOLE_1:12
.=
([#] X) /\ ([#] X)
by XBOOLE_1:12
.=
[#] X
;
hence
A1 /\ B1,A2 \/ B2 constitute_a_decomposition
by A6; verum