take {}
; :: thesis: ( {}in Sigma & ex C1 being thin of P st A ={}\/ C1 ) consider B2 being set such that A4:
B2 in Sigma
and A5:
ex C2 being thin of P st B = B2 \/ C2
byA1, Def5; A6:
P . B2 =0byA3, A4, A5, Def8; consider C2 being thin of P such that A7:
B = B2 \/ C2
byA5; set C1 = (A /\ B2)\/(A /\ C2); consider D2 being set such that A8:
D2 in Sigma
and A9:
C2 c= D2
and A10:
P . D2 =0byDef4; set O = B2 \/ D2;
A /\ C2 c= C2
byXBOOLE_1:17; then A11:
( A /\ B2 c= B2 & A /\ C2 c= D2 )
byA9, XBOOLE_1:17;
ex O being set st ( O in Sigma & (A /\ B2)\/(A /\ C2)c= O & P . O =0 )