reconsider C = {} as thin of P by Th24;
defpred S₁[ object , object ] means for x, y being set st x in COM (Sigma,P) & x = $1 & y = $2 holds
for B being set st B in Sigma holds
for C being thin of P st x = B \/ C holds
y = P . B;
set B = {} ;
A1: {} is thin of P by Th24;
A2: for x being object st x in COM (Sigma,P) holds
ex y being object st
( y in REAL & S₁[x,y] )

proof

let x be object ; :: thesis: ( x in COM (Sigma,P) implies ex y being object st
( y in REAL & S₁[x,y] ) )
assume x in COM (Sigma,P) ; :: thesis: ex y being object st
( y in REAL & S₁[x,y] )
then consider B being set such that
A3: ( B in Sigma & ex C being thin of P st x = B \/ C ) by Def5;
take P . B ; :: thesis: ( P . B in REAL & S₁[x,P . B] )
thus ( P . B in REAL & S₁[x,P . B] ) by A3, Th25, FUNCT_2:5; :: thesis: verum

end;

consider comP being Function of (COM (Sigma,P)),REAL such that
A4: for x being object st x in COM (Sigma,P) holds
S₁[x,comP . x] from FUNCT_2:sch 1(A2);
A5: for B being set st B in Sigma holds
for C being thin of P holds comP . (B \/ C) = P . B

proof

let B be set ; :: thesis: ( B in Sigma implies for C being thin of P holds comP . (B \/ C) = P . B )
assume A6: B in Sigma ; :: thesis: for C being thin of P holds comP . (B \/ C) = P . B
let C be thin of P; :: thesis: comP . (B \/ C) = P . B
B \/ C in COM (Sigma,P) by A6, Def5;
hence comP . (B \/ C) = P . B by A4, A6; :: thesis: verum

end;

A7: for BSeq being SetSequence of COM (Sigma,P) st BSeq is disjoint_valued holds
Sum (comP * BSeq) = comP . (Union BSeq)

proof

let BSeq be SetSequence of COM (Sigma,P); :: thesis: ( BSeq is disjoint_valued implies Sum (comP * BSeq) = comP . (Union BSeq) )
assume A8: BSeq is disjoint_valued ; :: thesis: Sum (comP * BSeq) = comP . (Union BSeq)
reconsider F = BSeq as sequence of (bool Omega) ;
rng F c= COM (Sigma,P) by RELAT_1:def 19;
then reconsider F = F as sequence of (COM (Sigma,P)) by FUNCT_2:6;
consider CSeq being SetSequence of Sigma such that
A9: for n being Element of NAT holds CSeq . n in ProbPart (F . n) by Th31;
consider B being set such that
A10: B = union (rng CSeq) ;
Union CSeq in Sigma by PROB_1:17;
then reconsider B = B as Element of Sigma by A10, CARD_3:def 4;
consider DSeq being SetSequence of Omega such that
A11: for n being Element of NAT holds DSeq . n = (F . n) \ (CSeq . n) by Th32;
A12: for n being Element of NAT holds
( CSeq . n in Sigma & CSeq . n c= F . n & (F . n) \ (CSeq . n) is thin of P )

proof

let n be Element of NAT ; :: thesis: ( CSeq . n in Sigma & CSeq . n c= F . n & (F . n) \ (CSeq . n) is thin of P )
CSeq . n in ProbPart (F . n) by A9;
hence ( CSeq . n in Sigma & CSeq . n c= F . n & (F . n) \ (CSeq . n) is thin of P ) by Def7; :: thesis: verum

end;

for n being Element of NAT holds DSeq . n is thin of P

proof

let n be Element of NAT ; :: thesis: DSeq . n is thin of P
(F . n) \ (CSeq . n) is thin of P by A12;
hence DSeq . n is thin of P by A11; :: thesis: verum

end;

then consider ESeq being SetSequence of Sigma such that
A13: for n being Element of NAT holds
( DSeq . n c= ESeq . n & P . (ESeq . n) = 0 ) by Th33;
A14: dom BSeq = NAT by FUNCT_2:def 1;
A15: B c= union (rng F)

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in B or x in union (rng F) )
assume x in B ; :: thesis: x in union (rng F)
then consider Z being set such that
A16: x in Z and
A17: Z in rng CSeq by A10, TARSKI:def 4;
dom CSeq = NAT by FUNCT_2:def 1;
then consider n being object such that
A18: n in NAT and
A19: Z = CSeq . n by A17, FUNCT_1:def 3;
reconsider n = n as Element of NAT by A18;
set P = F . n;
A20: CSeq . n c= F . n by A12;
ex P being set st
( P in rng F & x in P )

proof

take F . n ; :: thesis: ( F . n in rng F & x in F . n )
thus ( F . n in rng F & x in F . n ) by A14, A16, A19, A20, FUNCT_1:def 3; :: thesis: verum

end;

hence x in union (rng F) by TARSKI:def 4; :: thesis: verum

end;

A21: ex C being thin of P st union (rng F) = B \/ C

proof

set C = (union (rng F)) \ B;
A22: union (rng F) = ((union (rng F)) \ B) \/ ((union (rng F)) /\ B) by XBOOLE_1:51
.= B \/ ((union (rng F)) \ B) by A15, XBOOLE_1:28 ;
reconsider C = (union (rng F)) \ B as Subset of Omega ;
A23: C c= union (rng DSeq)

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in C or x in union (rng DSeq) )
assume A24: x in C ; :: thesis: x in union (rng DSeq)
then x in union (rng F) by XBOOLE_0:def 5;
then consider Z being set such that
A25: x in Z and
A26: Z in rng F by TARSKI:def 4;
consider n being object such that
A27: n in NAT and
A28: Z = F . n by A14, A26, FUNCT_1:def 3;
reconsider n = n as Element of NAT by A27;
A29: not x in union (rng CSeq) by A10, A24, XBOOLE_0:def 5;
not x in CSeq . n

proof

dom CSeq = NAT by FUNCT_2:def 1;
then A30: CSeq . n in rng CSeq by FUNCT_1:def 3;
assume x in CSeq . n ; :: thesis: contradiction
hence contradiction by A29, A30, TARSKI:def 4; :: thesis: verum

end;

then A31: x in (F . n) \ (CSeq . n) by A25, A28, XBOOLE_0:def 5;
ex Z being set st
( x in Z & Z in rng DSeq )

proof

take DSeq . n ; :: thesis: ( x in DSeq . n & DSeq . n in rng DSeq )
dom DSeq = NAT by FUNCT_2:def 1;
hence ( x in DSeq . n & DSeq . n in rng DSeq ) by A11, A31, FUNCT_1:def 3; :: thesis: verum

end;

hence x in union (rng DSeq) by TARSKI:def 4; :: thesis: verum

end;

for A being set st A in rng ESeq holds
P . A = 0

proof

let A be set ; :: thesis: ( A in rng ESeq implies P . A = 0 )
A32: dom ESeq = NAT by FUNCT_2:def 1;
assume A in rng ESeq ; :: thesis: P . A = 0
then ex n being object st
( n in NAT & A = ESeq . n ) by A32, FUNCT_1:def 3;
hence P . A = 0 by A13; :: thesis: verum

end;

then A33: P . (union (rng ESeq)) = 0 by Th8;
Union ESeq in Sigma by PROB_1:17;
then A34: union (rng ESeq) in Sigma by CARD_3:def 4;
union (rng DSeq) c= union (rng ESeq)

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in union (rng DSeq) or x in union (rng ESeq) )
assume x in union (rng DSeq) ; :: thesis: x in union (rng ESeq)
then consider Z being set such that
A35: x in Z and
A36: Z in rng DSeq by TARSKI:def 4;
dom DSeq = NAT by FUNCT_2:def 1;
then consider n being object such that
A37: n in NAT and
A38: Z = DSeq . n by A36, FUNCT_1:def 3;
reconsider n = n as Element of NAT by A37;
n in dom ESeq by A37, FUNCT_2:def 1;
then A39: ESeq . n in rng ESeq by FUNCT_1:def 3;
DSeq . n c= ESeq . n by A13;
hence x in union (rng ESeq) by A35, A38, A39, TARSKI:def 4; :: thesis: verum

end;

then C c= union (rng ESeq) by A23;
then C is thin of P by A34, A33, Def4;
then consider C being thin of P such that
A40: union (rng F) = B \/ C by A22;
take C ; :: thesis: union (rng F) = B \/ C
thus union (rng F) = B \/ C by A40; :: thesis: verum

end;

for n, m being object st n <> m holds
CSeq . n misses CSeq . m

proof

let n, m be object ; :: thesis: ( n <> m implies CSeq . n misses CSeq . m )
A41: dom F = NAT by FUNCT_2:def 1
.= dom CSeq by FUNCT_2:def 1 ;
for n being object holds CSeq . n c= F . n

proof

let n be object ; :: thesis: CSeq . n c= F . n

per cases ( n in dom F or not n in dom F ) ;

suppose n in dom F ; :: thesis: CSeq . n c= F . n

hence CSeq . n c= F . n by A12; :: thesis: verum

end;

suppose A42: not n in dom F ; :: thesis: CSeq . n c= F . n

then F . n = {} by FUNCT_1:def 2
.= CSeq . n by A41, A42, FUNCT_1:def 2 ;
hence CSeq . n c= F . n ; :: thesis: verum

end;

end;

end;

then A43: ( CSeq . n c= F . n & CSeq . m c= F . m ) ;
assume n <> m ; :: thesis: CSeq . n misses CSeq . m
then F . n misses F . m by A8, PROB_2:def 2;
then (F . n) /\ (F . m) = {} ;
then (CSeq . n) /\ (CSeq . m) = {} by A43, XBOOLE_1:3, XBOOLE_1:27;
hence CSeq . n misses CSeq . m ; :: thesis: verum

end;

then A44: CSeq is disjoint_valued ;
Sum (comP * F) = comP . (Union F)

proof

A45: for n being Element of NAT holds comP . (F . n) = P . (CSeq . n)

proof

let n be Element of NAT ; :: thesis: comP . (F . n) = P . (CSeq . n)
(F . n) \ (CSeq . n) is thin of P by A12;
then consider C being thin of P such that
A46: C = (F . n) \ (CSeq . n) ;
F . n = ((F . n) /\ (CSeq . n)) \/ ((F . n) \ (CSeq . n)) by XBOOLE_1:51
.= (CSeq . n) \/ C by A12, A46, XBOOLE_1:28 ;
hence comP . (F . n) = P . (CSeq . n) by A5; :: thesis: verum

end;

for x being Element of NAT holds (comP * F) . x = (P * CSeq) . x

proof

let x be Element of NAT ; :: thesis: (comP * F) . x = (P * CSeq) . x
(comP * F) . x = comP . (F . x) by FUNCT_2:15
.= P . (CSeq . x) by A45
.= (P * CSeq) . x by FUNCT_2:15 ;
hence (comP * F) . x = (P * CSeq) . x ; :: thesis: verum

end;

then A47: Sum (comP * F) = Sum (P * CSeq) by FUNCT_2:63;
comP . (union (rng F)) = P . (union (rng CSeq)) by A5, A10, A21;
then comP . (Union F) = P . (union (rng CSeq)) by CARD_3:def 4
.= P . (Union CSeq) by CARD_3:def 4 ;
hence Sum (comP * F) = comP . (Union F) by A44, A47, PROB_3:46; :: thesis: verum

end;

hence Sum (comP * BSeq) = comP . (Union BSeq) ; :: thesis: verum

end;

A48: for x being Element of COM (Sigma,P) holds comP . x >= 0

proof

let x be Element of COM (Sigma,P); :: thesis: comP . x >= 0
consider B being set such that
A49: B in Sigma and
A50: ex C being thin of P st x = B \/ C by Def5;
reconsider B = B as Element of Sigma by A49;
comP . x = P . B by A4, A50;
hence comP . x >= 0 by PROB_1:def 8; :: thesis: verum

end;

{} = {} \/ C ;
then A51: comP . {} = P . {} by A5, PROB_1:4
.= 0 by VALUED_0:def 19 ;
A52: for A, B being Event of COM (Sigma,P) st A misses B holds
comP . (A \/ B) = (comP . A) + (comP . B)

proof

let A, B be Event of COM (Sigma,P); :: thesis: ( A misses B implies comP . (A \/ B) = (comP . A) + (comP . B) )
assume A53: A misses B ; :: thesis: comP . (A \/ B) = (comP . A) + (comP . B)
reconsider A1 = A, B1 = B as Subset of Omega ;
reconsider BSeq = (A1,B1) followed_by ({} Omega) as SetSequence of Omega ;
A54: BSeq . 1 = B by FUNCT_7:123;
A55: BSeq . 0 = A by FUNCT_7:122;
for n being Nat holds BSeq . n in COM (Sigma,P)

proof

let n be Nat; :: thesis: BSeq . n in COM (Sigma,P)

per cases ( n = 0 or n <> 0 ) ;

suppose n = 0 ; :: thesis: BSeq . n in COM (Sigma,P)

hence BSeq . n in COM (Sigma,P) by A55; :: thesis: verum

end;

suppose n <> 0 ; :: thesis: BSeq . n in COM (Sigma,P)

then n >= 1 by NAT_1:14;
then A56: n + 1 > 1 by NAT_1:13;

per cases ( n > 1 or n = 1 ) by A56, NAT_1:22;

suppose n > 1 ; :: thesis: BSeq . n in COM (Sigma,P)

then BSeq . n = {} by FUNCT_7:124;
hence BSeq . n in COM (Sigma,P) by PROB_1:4; :: thesis: verum

end;

suppose n = 1 ; :: thesis: BSeq . n in COM (Sigma,P)

hence BSeq . n in COM (Sigma,P) by A54; :: thesis: verum

end;

end;

end;

end;

end;

then rng BSeq c= COM (Sigma,P) by NAT_1:52;
then reconsider BSeq = BSeq as SetSequence of COM (Sigma,P) by RELAT_1:def 19;
for m being Nat st 2 <= m holds
(Partial_Sums (comP * BSeq)) . m = (comP . A) + (comP . B)

proof

A57: (Partial_Sums (comP * BSeq)) . 0 = (comP * BSeq) . 0 by SERIES_1:def 1
.= comP . A by A55, FUNCT_2:15 ;
0 + 1 = 1 ;
then A58: (Partial_Sums (comP * BSeq)) . 1 = ((Partial_Sums (comP * BSeq)) . 0) + ((comP * BSeq) . 1) by SERIES_1:def 1
.= (comP . A) + (comP . B) by A54, A57, FUNCT_2:15 ;
A59: for n being Nat holds (Partial_Sums (comP * BSeq)) . (2 + n) = (comP . A) + (comP . B)

proof

defpred S₂[ Nat] means (Partial_Sums (comP * BSeq)) . (2 + $1) = (comP . A) + (comP . B);
A60: for k being Nat st S₂[k] holds
S₂[k + 1]

proof

let k be Nat; :: thesis: ( S₂[k] implies S₂[k + 1] )
assume A61: S₂[k] ; :: thesis: S₂[k + 1]
A62: (2 + k) + 1 > 0 + 1 by XREAL_1:8;
thus (Partial_Sums (comP * BSeq)) . (2 + (k + 1)) = ((Partial_Sums (comP * BSeq)) . (2 + k)) + ((comP * BSeq) . ((2 + k) + 1)) by SERIES_1:def 1
.= ((comP . A) + (comP . B)) + (comP . (BSeq . ((2 + k) + 1))) by A61, FUNCT_2:15
.= ((comP . A) + (comP . B)) + (comP . {}) by A62, FUNCT_7:124
.= (comP . A) + (comP . B) by A51 ; :: thesis: verum

end;

2 = 1 + 1 ;
then (Partial_Sums (comP * BSeq)) . (2 + 0) = ((Partial_Sums (comP * BSeq)) . 1) + ((comP * BSeq) . 2) by SERIES_1:def 1
.= ((comP . A) + (comP . B)) + (comP . (BSeq . 2)) by A58, FUNCT_2:15
.= ((comP . A) + (comP . B)) + (comP . {}) by FUNCT_7:124
.= (comP . A) + (comP . B) by A51 ;
then A63: S₂[ 0 ] ;
thus for k being Nat holds S₂[k] from NAT_1:sch 2(A63, A60); :: thesis: verum

end;

let m be Nat; :: thesis: ( 2 <= m implies (Partial_Sums (comP * BSeq)) . m = (comP . A) + (comP . B) )
assume 2 <= m ; :: thesis: (Partial_Sums (comP * BSeq)) . m = (comP . A) + (comP . B)
then consider k being Nat such that
A64: m = 2 + k by NAT_1:10;
thus (Partial_Sums (comP * BSeq)) . m = (comP . A) + (comP . B) by A59, A64; :: thesis: verum

end;

then A65: ( Union BSeq = A \/ B & Sum (comP * BSeq) = (comP . A) + (comP . B) ) by DYNKIN:3, PROB_1:1;
BSeq is disjoint_valued by A53, Th3;
hence comP . (A \/ B) = (comP . A) + (comP . B) by A7, A65; :: thesis: verum

end;

A66: for A, B being Event of COM (Sigma,P) st A c= B holds
comP . (B \ A) = (comP . B) - (comP . A)

proof

let A, B be Event of COM (Sigma,P); :: thesis: ( A c= B implies comP . (B \ A) = (comP . B) - (comP . A) )
assume A67: A c= B ; :: thesis: comP . (B \ A) = (comP . B) - (comP . A)
(comP . A) + (comP . (B \ A)) = comP . (A \/ (B \ A)) by A52, XBOOLE_1:79
.= comP . B by A67, XBOOLE_1:45 ;
hence comP . (B \ A) = (comP . B) - (comP . A) ; :: thesis: verum

end;

A68: for A, B being Event of COM (Sigma,P) st A c= B holds
comP . A <= comP . B

proof

let A, B be Event of COM (Sigma,P); :: thesis: ( A c= B implies comP . A <= comP . B )
assume A c= B ; :: thesis: comP . A <= comP . B
then comP . (B \ A) = (comP . B) - (comP . A) by A66;
then 0 <= (comP . B) - (comP . A) by A48;
then 0 + (comP . A) <= comP . B by XREAL_1:19;
hence comP . A <= comP . B ; :: thesis: verum

end;

A69: for BSeq being SetSequence of COM (Sigma,P) st BSeq is non-descending holds
comP * BSeq is non-decreasing

proof

let BSeq be SetSequence of COM (Sigma,P); :: thesis: ( BSeq is non-descending implies comP * BSeq is non-decreasing )
assume A70: BSeq is non-descending ; :: thesis: comP * BSeq is non-decreasing
for n, m being Nat st n <= m holds
(comP * BSeq) . n <= (comP * BSeq) . m

proof

let n, m be Nat; :: thesis: ( n <= m implies (comP * BSeq) . n <= (comP * BSeq) . m )
A71: ( n in NAT & m in NAT ) by ORDINAL1:def 12;
assume n <= m ; :: thesis: (comP * BSeq) . n <= (comP * BSeq) . m
then BSeq . n c= BSeq . m by A70, PROB_1:def 5;
then comP . (BSeq . n) <= comP . (BSeq . m) by A68;
then (comP * BSeq) . n <= comP . (BSeq . m) by FUNCT_2:15, A71;
hence (comP * BSeq) . n <= (comP * BSeq) . m by FUNCT_2:15, A71; :: thesis: verum

end;

hence comP * BSeq is non-decreasing by SEQM_3:6; :: thesis: verum

end;

A72: comP . Omega = comP . ({} \/ Omega)
.= P . Omega by A5, A1, PROB_1:5
.= 1 by PROB_1:def 8 ;
A73: for A being Event of COM (Sigma,P) holds comP . A <= 1

proof

reconsider B = Omega as Event of COM (Sigma,P) by PROB_1:23;
let A be Event of COM (Sigma,P); :: thesis: comP . A <= 1
comP . A <= comP . B by A68;
hence comP . A <= 1 by A72; :: thesis: verum

end;

A74: for BSeq being SetSequence of COM (Sigma,P)
for n being Element of NAT holds (comP * BSeq) . n <= 1

proof

let BSeq be SetSequence of COM (Sigma,P); :: thesis: for n being Element of NAT holds (comP * BSeq) . n <= 1
let n be Element of NAT ; :: thesis: (comP * BSeq) . n <= 1
(comP * BSeq) . n = comP . (BSeq . n) by FUNCT_2:15;
hence (comP * BSeq) . n <= 1 by A73; :: thesis: verum

end;

A75: for BSeq being SetSequence of COM (Sigma,P) st BSeq is non-descending holds
( comP * BSeq is bounded_above & comP * BSeq is convergent )

proof

let BSeq be SetSequence of COM (Sigma,P); :: thesis: ( BSeq is non-descending implies ( comP * BSeq is bounded_above & comP * BSeq is convergent ) )
assume BSeq is non-descending ; :: thesis: ( comP * BSeq is bounded_above & comP * BSeq is convergent )
then A76: comP * BSeq is non-decreasing by A69;
for n being Nat holds (comP * BSeq) . n < 2

proof

let n be Nat; :: thesis: (comP * BSeq) . n < 2
n in NAT by ORDINAL1:def 12;
then ((comP * BSeq) . n) + 0 < 1 + 1 by A74, XREAL_1:8;
hence (comP * BSeq) . n < 2 ; :: thesis: verum

end;

hence comP * BSeq is bounded_above by SEQ_2:def 3; :: thesis: comP * BSeq is convergent
hence comP * BSeq is convergent by A76; :: thesis: verum

end;

for BSeq being SetSequence of COM (Sigma,P) st BSeq is non-descending holds
( comP * BSeq is convergent & lim (comP * BSeq) = comP . (Union BSeq) )

proof

let BSeq be SetSequence of COM (Sigma,P); :: thesis: ( BSeq is non-descending implies ( comP * BSeq is convergent & lim (comP * BSeq) = comP . (Union BSeq) ) )
assume A77: BSeq is non-descending ; :: thesis: ( comP * BSeq is convergent & lim (comP * BSeq) = comP . (Union BSeq) )
reconsider CSeq = Partial_Diff_Union BSeq as SetSequence of COM (Sigma,P) ;
A78: for n being Nat holds (Partial_Sums (comP * CSeq)) . n = (comP * BSeq) . n

proof

defpred S₂[ Nat] means (Partial_Sums (comP * CSeq)) . $1 = (comP * BSeq) . $1;
A79: for k being Nat st S₂[k] holds
S₂[k + 1]

proof

let k be Nat; :: thesis: ( S₂[k] implies S₂[k + 1] )
assume A80: S₂[k] ; :: thesis: S₂[k + 1]
A81: BSeq . k c= BSeq . (k + 1) by A77, PROB_2:7;
reconsider kk = k as Element of NAT by ORDINAL1:def 12;
thus (Partial_Sums (comP * CSeq)) . (k + 1) = ((comP * BSeq) . kk) + ((comP * CSeq) . (k + 1)) by A80, SERIES_1:def 1
.= (comP . (BSeq . kk)) + ((comP * CSeq) . (k + 1)) by FUNCT_2:15
.= (comP . (BSeq . k)) + (comP . (CSeq . (k + 1))) by FUNCT_2:15
.= comP . ((BSeq . k) \/ (CSeq . (k + 1))) by A52, A77, Th18
.= comP . ((BSeq . k) \/ ((BSeq . (k + 1)) \ (BSeq . k))) by A77, Th16
.= comP . ((BSeq . k) \/ (BSeq . (k + 1))) by XBOOLE_1:39
.= comP . (BSeq . (k + 1)) by A81, XBOOLE_1:12
.= (comP * BSeq) . (k + 1) by FUNCT_2:15 ; :: thesis: verum

end;

(Partial_Sums (comP * CSeq)) . 0 = (comP * CSeq) . 0 by SERIES_1:def 1
.= comP . (CSeq . 0) by FUNCT_2:15
.= comP . (BSeq . 0) by A77, Th16
.= (comP * BSeq) . 0 by FUNCT_2:15 ;
then A82: S₂[ 0 ] ;
thus for k being Nat holds S₂[k] from NAT_1:sch 2(A82, A79); :: thesis: verum

end;

A83: Partial_Sums (comP * CSeq) = comP * BSeq by A78;
comP . (Union BSeq) = comP . (Union CSeq) by PROB_3:36
.= Sum (comP * CSeq) by A7
.= lim (Partial_Sums (comP * CSeq)) ;
hence ( comP * BSeq is convergent & lim (comP * BSeq) = comP . (Union BSeq) ) by A75, A77, A83; :: thesis: verum

end;

then reconsider comP = comP as Probability of COM (Sigma,P) by A48, A72, A52, PROB_2:10;
take comP ; :: thesis: for B being set st B in Sigma holds
for C being thin of P holds comP . (B \/ C) = P . B
thus for B being set st B in Sigma holds
for C being thin of P holds comP . (B \/ C) = P . B by A5; :: thesis: verum