:: RPR_1 semantic presentation  Show TPTP formulae Show IDV graph for whole article:: Showing IDV graph ... (Click the Palm Trees again to close it)

registration
let E be non empty set ;
cluster non empty trivial Element of K16(E);
existence
ex b1 being Subset of E st
( not b1 is empty & b1 is trivial )
proof end;
end;

definition
let E be non empty set ;
mode El_ev of E is non empty trivial Subset of E;
end;

theorem Th1: :: RPR_1:1  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for E being non empty set
for e being non empty Subset of E holds
( e is El_ev of E iff for Y being set holds
( Y c= e iff ( Y = {} or Y = e ) ) )
proof end;

registration
let E be non empty set ;
cluster -> finite Element of K16(E);
coherence
for b1 being El_ev of E holds b1 is finite
proof end;
end;

theorem :: RPR_1:2  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: RPR_1:3  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: RPR_1:4  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: RPR_1:5  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for E being non empty set
for A, B being Subset of E
for e being El_ev of E st e = A \/ B & A <> B & not ( A = {} & B = e ) holds
( A = e & B = {} )
proof end;

theorem :: RPR_1:6  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for E being non empty set
for A, B being Subset of E
for e being El_ev of E holds
( not e = A \/ B or ( A = e & B = e ) or ( A = e & B = {} ) or ( A = {} & B = e ) )
proof end;

theorem Th7: :: RPR_1:7  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for E being non empty set
for a being Element of E holds {a} is El_ev of E
proof end;

theorem :: RPR_1:8  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: RPR_1:9  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: RPR_1:10  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for E being non empty set
for e1, e2 being El_ev of E st e1 c= e2 holds
e1 = e2 by Th1;

theorem Th11: :: RPR_1:11  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for E being non empty set
for e being El_ev of E ex a being Element of E st
( a in E & e = {a} )
proof end;

theorem :: RPR_1:12  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for E being non empty set ex e being El_ev of E st e is El_ev of E
proof end;

theorem :: RPR_1:13  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: RPR_1:14  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for E being non empty set
for e being El_ev of E ex p being FinSequence st
( p is FinSequence of E & rng p = e & len p = 1 )
proof end;

definition
let E be set ;
mode Event of E is Subset of E;
end;

theorem :: RPR_1:15  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: RPR_1:16  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: RPR_1:17  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: RPR_1:18  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: RPR_1:19  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: RPR_1:20  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: RPR_1:21  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: RPR_1:22  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for E being non empty set
for e being El_ev of E
for A being Event of E holds
( e misses A or e /\ A = e )
proof end;

theorem :: RPR_1:23  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: RPR_1:24  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: RPR_1:25  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for E being non empty set
for A being Event of E st A <> {} holds
ex e being El_ev of E st e c= A
proof end;

theorem :: RPR_1:26  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for E being non empty set
for e being El_ev of E
for A being Event of E holds
( not e c= A \/ (A ` ) or e c= A or e c= A ` )
proof end;

theorem :: RPR_1:27  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for E being non empty set
for e1, e2 being El_ev of E holds
( e1 = e2 or e1 misses e2 )
proof end;

theorem :: RPR_1:28  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: RPR_1:29  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: RPR_1:30  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: RPR_1:31  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: RPR_1:32  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: RPR_1:33  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th34: :: RPR_1:34  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for E being non empty set
for A, B being Subset of E holds A /\ B misses A /\ (B ` )
proof end;

Lm1: for E being non empty finite set holds 0 < card E
proof end;

Lm2: for E being non empty set
for e being El_ev of E holds card e = 1
proof end;

definition
let E be non empty finite set ;
let A be Event of E;
canceled;
canceled;
canceled;
func prob A -> Real equals :: RPR_1:def 4
(card A) / (card E);
coherence
(card A) / (card E) is Real
;
end;

:: deftheorem RPR_1:def 1 :
canceled;

:: deftheorem RPR_1:def 2 :
canceled;

:: deftheorem RPR_1:def 3 :
canceled;

:: deftheorem defines prob RPR_1:def 4 :
for E being non empty finite set
for A being Event of E holds prob A = (card A) / (card E);

theorem :: RPR_1:35  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: RPR_1:36  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: RPR_1:37  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: RPR_1:38  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for E being non empty finite set
for e being El_ev of E holds prob e = 1 / (card E) by Lm2;

theorem Th39: :: RPR_1:39  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for E being non empty finite set holds prob ([#] E) = 1
proof end;

theorem Th40: :: RPR_1:40  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for E being non empty finite set holds prob ({} E) = 0 by CARD_1:78;

theorem Th41: :: RPR_1:41  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for E being non empty finite set
for A, B being Event of E st A misses B holds
prob (A /\ B) = 0
proof end;

theorem :: RPR_1:42  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for E being non empty finite set
for A being Event of E holds prob A <= 1
proof end;

theorem Th43: :: RPR_1:43  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for E being non empty finite set
for A being Event of E holds 0 <= prob A
proof end;

theorem Th44: :: RPR_1:44  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for E being non empty finite set
for A, B being Event of E st A c= B holds
prob A <= prob B
proof end;

theorem :: RPR_1:45  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th46: :: RPR_1:46  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for E being non empty finite set
for A, B being Event of E holds prob (A \/ B) = ((prob A) + (prob B)) - (prob (A /\ B))
proof end;

theorem Th47: :: RPR_1:47  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for E being non empty finite set
for A, B being Event of E st A misses B holds
prob (A \/ B) = (prob A) + (prob B)
proof end;

theorem Th48: :: RPR_1:48  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for E being non empty finite set
for A being Event of E holds
( prob A = 1 - (prob (A ` )) & prob (A ` ) = 1 - (prob A) )
proof end;

theorem Th49: :: RPR_1:49  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for E being non empty finite set
for A, B being Event of E holds prob (A \ B) = (prob A) - (prob (A /\ B))
proof end;

theorem Th50: :: RPR_1:50  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for E being non empty finite set
for A, B being Event of E st B c= A holds
prob (A \ B) = (prob A) - (prob B)
proof end;

theorem :: RPR_1:51  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for E being non empty finite set
for A, B being Event of E holds prob (A \/ B) <= (prob A) + (prob B)
proof end;

theorem :: RPR_1:52  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th53: :: RPR_1:53  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for E being non empty finite set
for A, B being Event of E holds prob A = (prob (A /\ B)) + (prob (A /\ (B ` )))
proof end;

theorem :: RPR_1:54  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for E being non empty finite set
for A, B being Event of E holds prob A = (prob (A \/ B)) - (prob (B \ A))
proof end;

theorem :: RPR_1:55  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for E being non empty finite set
for A, B being Event of E holds (prob A) + (prob ((A ` ) /\ B)) = (prob B) + (prob ((B ` ) /\ A))
proof end;

theorem Th56: :: RPR_1:56  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for E being non empty finite set
for A, B, C being Event of E holds prob ((A \/ B) \/ C) = ((((prob A) + (prob B)) + (prob C)) - (((prob (A /\ B)) + (prob (A /\ C))) + (prob (B /\ C)))) + (prob ((A /\ B) /\ C))
proof end;

theorem :: RPR_1:57  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for E being non empty finite set
for A, B, C being Event of E st A misses B & A misses C & B misses C holds
prob ((A \/ B) \/ C) = ((prob A) + (prob B)) + (prob C)
proof end;

theorem :: RPR_1:58  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for E being non empty finite set
for A, B being Event of E holds (prob A) - (prob B) <= prob (A \ B)
proof end;

definition
let E be non empty finite set ;
let B, A be Event of E;
func prob A,B -> Real equals :: RPR_1:def 5
(prob (A /\ B)) / (prob B);
coherence
(prob (A /\ B)) / (prob B) is Real
;
end;

:: deftheorem defines prob RPR_1:def 5 :
for E being non empty finite set
for B, A being Event of E holds prob A,B = (prob (A /\ B)) / (prob B);

theorem :: RPR_1:59  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th60: :: RPR_1:60  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for E being non empty finite set
for A, B being Event of E st 0 < prob B holds
prob (A /\ B) = (prob A,B) * (prob B) by XCMPLX_1:88;

theorem Th61: :: RPR_1:61  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for E being non empty finite set
for A being Event of E holds prob A,([#] E) = prob A
proof end;

theorem :: RPR_1:62  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for E being non empty finite set holds prob ([#] E),([#] E) = 1
proof end;

theorem :: RPR_1:63  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for E being non empty finite set holds prob ({} E),([#] E) = 0
proof end;

theorem :: RPR_1:64  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for E being non empty finite set
for A, B being Event of E st 0 < prob B holds
prob A,B <= 1
proof end;

theorem :: RPR_1:65  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for E being non empty finite set
for A, B being Event of E st 0 < prob B holds
0 <= prob A,B
proof end;

theorem Th66: :: RPR_1:66  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for E being non empty finite set
for A, B being Event of E st 0 < prob B holds
prob A,B = 1 - ((prob (B \ A)) / (prob B))
proof end;

theorem :: RPR_1:67  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for E being non empty finite set
for A, B being Event of E st 0 < prob B & A c= B holds
prob A,B = (prob A) / (prob B)
proof end;

theorem Th68: :: RPR_1:68  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for E being non empty finite set
for A, B being Event of E st A misses B holds
prob A,B = 0
proof end;

theorem Th69: :: RPR_1:69  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for E being non empty finite set
for A, B being Event of E st 0 < prob A & 0 < prob B holds
(prob A) * (prob B,A) = (prob B) * (prob A,B)
proof end;

theorem Th70: :: RPR_1:70  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for E being non empty finite set
for A, B being Event of E st 0 < prob B holds
( prob A,B = 1 - (prob (A ` ),B) & prob (A ` ),B = 1 - (prob A,B) )
proof end;

theorem Th71: :: RPR_1:71  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for E being non empty finite set
for A, B being Event of E st 0 < prob B & B c= A holds
prob A,B = 1
proof end;

theorem :: RPR_1:72  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for E being non empty finite set
for B being Event of E st 0 < prob B holds
prob ([#] E),B = 1
proof end;

theorem :: RPR_1:73  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for E being non empty finite set
for A being Event of E st 0 < prob A holds
prob (A ` ),A = 0
proof end;

theorem :: RPR_1:74  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for E being non empty finite set
for A being Event of E st prob A < 1 holds
prob A,(A ` ) = 0
proof end;

theorem Th75: :: RPR_1:75  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for E being non empty finite set
for A, B being Event of E st 0 < prob B & A misses B holds
prob (A ` ),B = 1
proof end;

theorem Th76: :: RPR_1:76  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for E being non empty finite set
for A, B being Event of E st 0 < prob A & prob B < 1 & A misses B holds
prob A,(B ` ) = (prob A) / (1 - (prob B))
proof end;

theorem :: RPR_1:77  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for E being non empty finite set
for A, B being Event of E st 0 < prob A & prob B < 1 & A misses B holds
prob (A ` ),(B ` ) = 1 - ((prob A) / (1 - (prob B)))
proof end;

theorem :: RPR_1:78  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for E being non empty finite set
for A, B, C being Event of E st 0 < prob (B /\ C) & 0 < prob C holds
prob ((A /\ B) /\ C) = ((prob A,(B /\ C)) * (prob B,C)) * (prob C)
proof end;

theorem Th79: :: RPR_1:79  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for E being non empty finite set
for A, B being Event of E st 0 < prob B & prob B < 1 holds
prob A = ((prob A,B) * (prob B)) + ((prob A,(B ` )) * (prob (B ` )))
proof end;

theorem Th80: :: RPR_1:80  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for E being non empty finite set
for A, B1, B2 being Event of E st 0 < prob B1 & 0 < prob B2 & B1 \/ B2 = E & B1 misses B2 holds
prob A = ((prob A,B1) * (prob B1)) + ((prob A,B2) * (prob B2))
proof end;

theorem Th81: :: RPR_1:81  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for E being non empty finite set
for A, B1, B2, B3 being Event of E st 0 < prob B1 & 0 < prob B2 & 0 < prob B3 & (B1 \/ B2) \/ B3 = E & B1 misses B2 & B1 misses B3 & B2 misses B3 holds
prob A = (((prob A,B1) * (prob B1)) + ((prob A,B2) * (prob B2))) + ((prob A,B3) * (prob B3))
proof end;

theorem :: RPR_1:82  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for E being non empty finite set
for A, B1, B2 being Event of E st 0 < prob B1 & 0 < prob B2 & B1 \/ B2 = E & B1 misses B2 holds
prob B1,A = ((prob A,B1) * (prob B1)) / (((prob A,B1) * (prob B1)) + ((prob A,B2) * (prob B2)))
proof end;

theorem :: RPR_1:83  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for E being non empty finite set
for A, B1, B2, B3 being Event of E st 0 < prob B1 & 0 < prob B2 & 0 < prob B3 & (B1 \/ B2) \/ B3 = E & B1 misses B2 & B1 misses B3 & B2 misses B3 holds
prob B1,A = ((prob A,B1) * (prob B1)) / ((((prob A,B1) * (prob B1)) + ((prob A,B2) * (prob B2))) + ((prob A,B3) * (prob B3)))
proof end;

definition
let E be non empty finite set ;
let A, B be Event of E;
pred A,B are_independent means :Def6: :: RPR_1:def 6
prob (A /\ B) = (prob A) * (prob B);
symmetry
for A, B being Event of E st prob (A /\ B) = (prob A) * (prob B) holds
prob (B /\ A) = (prob B) * (prob A)
;
end;

:: deftheorem Def6 defines are_independent RPR_1:def 6 :
for E being non empty finite set
for A, B being Event of E holds
( A,B are_independent iff prob (A /\ B) = (prob A) * (prob B) );

theorem :: RPR_1:84  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: RPR_1:85  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: RPR_1:86  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for E being non empty finite set
for A, B being Event of E st 0 < prob B & A,B are_independent holds
prob A,B = prob A
proof end;

theorem :: RPR_1:87  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for E being non empty finite set
for A, B being Event of E st prob B = 0 holds
A,B are_independent
proof end;

theorem :: RPR_1:88  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for E being non empty finite set
for A, B being Event of E st A,B are_independent holds
A ` ,B are_independent
proof end;

theorem :: RPR_1:89  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for E being non empty finite set
for A, B being Event of E st A misses B & A,B are_independent & not prob A = 0 holds
prob B = 0
proof end;