PROB_2

:: PROB_2 semantic presentation

begin

for r, r1, r2, r3 being ( ( ) ( ext-real V14() real ) Real) st r : ( ( ) ( ext-real V14() real ) Real) <> 0 : ( ( ) ( ext-real non positive non negative empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V14() real V33() V34() V45() V46() V47() V48() V49() V50() V51() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) ) & r1 : ( ( ) ( ext-real V14() real ) Real) <> 0 : ( ( ) ( ext-real non positive non negative empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V14() real V33() V34() V45() V46() V47() V48() V49() V50() V51() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) ) holds
( r3 : ( ( ) ( ext-real V14() real ) Real) / r1 : ( ( ) ( ext-real V14() real ) Real) : ( ( ) ( ext-real V14() real ) Element of REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) = r2 : ( ( ) ( ext-real V14() real ) Real) / r : ( ( ) ( ext-real V14() real ) Real) : ( ( ) ( ext-real V14() real ) Element of REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) iff r3 : ( ( ) ( ext-real V14() real ) Real) * r : ( ( ) ( ext-real V14() real ) Real) : ( ( ) ( ext-real V14() real ) Element of REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) = r2 : ( ( ) ( ext-real V14() real ) Real) * r1 : ( ( ) ( ext-real V14() real ) Real) : ( ( ) ( ext-real V14() real ) Element of REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) ) ;

theorem :: PROB_2:2

for r being ( ( ) ( ext-real V14() real ) Real)
for seq, seq1 being ( ( Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) , REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) -valued Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) , REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) V35() V36() V37() ) Real_Sequence) st seq : ( ( Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) , REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) -valued Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) , REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) V35() V36() V37() ) Real_Sequence) is convergent & ( for n being ( ( ) ( ext-real epsilon-transitive epsilon-connected ordinal natural V14() real V33() V34() V45() V46() V47() V48() V49() V50() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) ) holds seq1 : ( ( Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) , REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) -valued Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) , REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) V35() V36() V37() ) Real_Sequence) . n : ( ( ) ( ext-real epsilon-transitive epsilon-connected ordinal natural V14() real V33() V34() V45() V46() V47() V48() V49() V50() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ext-real V14() real ) Element of REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) = r : ( ( ) ( ext-real V14() real ) Real) - (seq : ( ( Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) , REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) -valued Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) , REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) V35() V36() V37() ) Real_Sequence) . n : ( ( ) ( ext-real epsilon-transitive epsilon-connected ordinal natural V14() real V33() V34() V45() V46() V47() V48() V49() V50() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( ext-real V14() real ) Element of REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ext-real V14() real ) Element of REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) ) holds
( seq1 : ( ( Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) , REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) -valued Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) , REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) V35() V36() V37() ) Real_Sequence) is convergent & lim seq1 : ( ( Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) , REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) -valued Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) , REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) V35() V36() V37() ) Real_Sequence) : ( ( ) ( ext-real V14() real ) Element of REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) = r : ( ( ) ( ext-real V14() real ) Real) - (lim seq : ( ( Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) , REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) -valued Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) , REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) V35() V36() V37() ) Real_Sequence) ) : ( ( ) ( ext-real V14() real ) Element of REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ext-real V14() real ) Element of REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) ) ;

definition

let Omega be ( ( ) ( ) set ) ;
let Sigma be ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) SigmaField of Omega : ( ( ) ( ) set ) ) ;
let ASeq be ( ( Sigma : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) SigmaField of Omega : ( ( ) ( ) set ) ) -valued Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) ,K231(Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) -defined Sigma : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) SigmaField of Omega : ( ( ) ( ) set ) ) -valued K231(Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) ,K231(Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) SetSequence of Sigma : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) SigmaField of Omega : ( ( ) ( ) set ) ) ) ;
let n be ( ( ) ( ext-real epsilon-transitive epsilon-connected ordinal natural V14() real V33() V34() V45() V46() V47() V48() V49() V50() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) ) ;
:: original: .
redefine func ASeq . n -> ( ( ) ( ) Event of Sigma : ( ( ext-real ) ( ext-real ) set ) ) ;

end;

definition

func @Intersection ASeq -> ( ( ) ( ) Event of Sigma : ( ( ext-real ) ( ext-real ) set ) ) equals :: PROB_2:def 1
Intersection ASeq : ( ( ) ( ) set ) : ( ( ) ( ) Element of bool Omega : ( ( ext-real ) ( ext-real ) set ) : ( ( ) ( non empty ) set ) ) ;

end;

theorem :: PROB_2:3

for Omega being ( ( ) ( ) set )
for Sigma being ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) SigmaField of Omega : ( ( ) ( ) set ) )
for ASeq being ( ( b₂ : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) SigmaField of b₁ : ( ( ) ( ) set ) ) -valued Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) ,K231(b₁ : ( ( ) ( ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool b₁ : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) -defined b₂ : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) SigmaField of b₁ : ( ( ) ( ) set ) ) -valued K231(b₁ : ( ( ) ( ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool b₁ : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) ,K231(b₁ : ( ( ) ( ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool b₁ : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) SetSequence of Sigma : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) SigmaField of b₁ : ( ( ) ( ) set ) ) )
for B being ( ( ) ( ) Event of Sigma : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) SigmaField of b₁ : ( ( ) ( ) set ) ) ) ex BSeq being ( ( b₂ : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) SigmaField of b₁ : ( ( ) ( ) set ) ) -valued Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) ,K231(b₁ : ( ( ) ( ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool b₁ : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) -defined b₂ : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) SigmaField of b₁ : ( ( ) ( ) set ) ) -valued K231(b₁ : ( ( ) ( ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool b₁ : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) ,K231(b₁ : ( ( ) ( ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool b₁ : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) SetSequence of Sigma : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) SigmaField of b₁ : ( ( ) ( ) set ) ) ) st
for n being ( ( ) ( ext-real epsilon-transitive epsilon-connected ordinal natural V14() real V33() V34() V45() V46() V47() V48() V49() V50() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) ) holds BSeq : ( ( b₂ : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) SigmaField of b₁ : ( ( ) ( ) set ) ) -valued Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) ,K231(b₁ : ( ( ) ( ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool b₁ : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) -defined b₂ : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) SigmaField of b₁ : ( ( ) ( ) set ) ) -valued K231(b₁ : ( ( ) ( ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool b₁ : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) ,K231(b₁ : ( ( ) ( ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool b₁ : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) SetSequence of b₂ : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) SigmaField of b₁ : ( ( ) ( ) set ) ) ) . n : ( ( ) ( ext-real epsilon-transitive epsilon-connected ordinal natural V14() real V33() V34() V45() V46() V47() V48() V49() V50() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Event of b₂ : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) SigmaField of b₁ : ( ( ) ( ) set ) ) ) = (ASeq : ( ( b₂ : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) SigmaField of b₁ : ( ( ) ( ) set ) ) -valued Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) ,K231(b₁ : ( ( ) ( ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool b₁ : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) -defined b₂ : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) SigmaField of b₁ : ( ( ) ( ) set ) ) -valued K231(b₁ : ( ( ) ( ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool b₁ : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) ,K231(b₁ : ( ( ) ( ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool b₁ : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) SetSequence of b₂ : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) SigmaField of b₁ : ( ( ) ( ) set ) ) ) . n : ( ( ) ( ext-real epsilon-transitive epsilon-connected ordinal natural V14() real V33() V34() V45() V46() V47() V48() V49() V50() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( ) Event of b₂ : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) SigmaField of b₁ : ( ( ) ( ) set ) ) ) /\ B : ( ( ) ( ) Event of b₂ : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) SigmaField of b₁ : ( ( ) ( ) set ) ) ) : ( ( ) ( ) Event of b₂ : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) SigmaField of b₁ : ( ( ) ( ) set ) ) ) ;

theorem :: PROB_2:4

for Omega being ( ( ) ( ) set )
for Sigma being ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) SigmaField of Omega : ( ( ) ( ) set ) )
for ASeq, BSeq being ( ( b₂ : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) SigmaField of b₁ : ( ( ) ( ) set ) ) -valued Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) ,K231(b₁ : ( ( ) ( ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool b₁ : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) -defined b₂ : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) SigmaField of b₁ : ( ( ) ( ) set ) ) -valued K231(b₁ : ( ( ) ( ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool b₁ : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) ,K231(b₁ : ( ( ) ( ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool b₁ : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) SetSequence of Sigma : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) SigmaField of b₁ : ( ( ) ( ) set ) ) )
for B being ( ( ) ( ) Event of Sigma : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) SigmaField of b₁ : ( ( ) ( ) set ) ) ) st ASeq : ( ( b₂ : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) SigmaField of b₁ : ( ( ) ( ) set ) ) -valued Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) ,K231(b₁ : ( ( ) ( ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool b₁ : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) -defined b₂ : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) SigmaField of b₁ : ( ( ) ( ) set ) ) -valued K231(b₁ : ( ( ) ( ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool b₁ : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) ,K231(b₁ : ( ( ) ( ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool b₁ : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) SetSequence of b₂ : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) SigmaField of b₁ : ( ( ) ( ) set ) ) ) is non-ascending & ( for n being ( ( ) ( ext-real epsilon-transitive epsilon-connected ordinal natural V14() real V33() V34() V45() V46() V47() V48() V49() V50() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) ) holds BSeq : ( ( b₂ : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) SigmaField of b₁ : ( ( ) ( ) set ) ) -valued Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) ,K231(b₁ : ( ( ) ( ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool b₁ : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) -defined b₂ : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) SigmaField of b₁ : ( ( ) ( ) set ) ) -valued K231(b₁ : ( ( ) ( ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool b₁ : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) ,K231(b₁ : ( ( ) ( ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool b₁ : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) SetSequence of b₂ : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) SigmaField of b₁ : ( ( ) ( ) set ) ) ) . n : ( ( ) ( ext-real epsilon-transitive epsilon-connected ordinal natural V14() real V33() V34() V45() V46() V47() V48() V49() V50() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Event of b₂ : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) SigmaField of b₁ : ( ( ) ( ) set ) ) ) = (ASeq : ( ( b₂ : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) SigmaField of b₁ : ( ( ) ( ) set ) ) -valued Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) ,K231(b₁ : ( ( ) ( ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool b₁ : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) -defined b₂ : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) SigmaField of b₁ : ( ( ) ( ) set ) ) -valued K231(b₁ : ( ( ) ( ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool b₁ : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) ,K231(b₁ : ( ( ) ( ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool b₁ : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) SetSequence of b₂ : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) SigmaField of b₁ : ( ( ) ( ) set ) ) ) . n : ( ( ) ( ext-real epsilon-transitive epsilon-connected ordinal natural V14() real V33() V34() V45() V46() V47() V48() V49() V50() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( ) Event of b₂ : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) SigmaField of b₁ : ( ( ) ( ) set ) ) ) /\ B : ( ( ) ( ) Event of b₂ : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) SigmaField of b₁ : ( ( ) ( ) set ) ) ) : ( ( ) ( ) Event of b₂ : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) SigmaField of b₁ : ( ( ) ( ) set ) ) ) ) holds
BSeq : ( ( b₂ : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) SigmaField of b₁ : ( ( ) ( ) set ) ) -valued Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) ,K231(b₁ : ( ( ) ( ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool b₁ : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) -defined b₂ : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) SigmaField of b₁ : ( ( ) ( ) set ) ) -valued K231(b₁ : ( ( ) ( ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool b₁ : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) ,K231(b₁ : ( ( ) ( ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool b₁ : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) SetSequence of b₂ : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) SigmaField of b₁ : ( ( ) ( ) set ) ) ) is non-ascending ;

theorem :: PROB_2:5

for Omega being ( ( ) ( ) set )
for Sigma being ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) SigmaField of Omega : ( ( ) ( ) set ) )
for BSeq, ASeq being ( ( b₂ : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) SigmaField of b₁ : ( ( ) ( ) set ) ) -valued Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) ,K231(b₁ : ( ( ) ( ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool b₁ : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) -defined b₂ : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) SigmaField of b₁ : ( ( ) ( ) set ) ) -valued K231(b₁ : ( ( ) ( ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool b₁ : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) ,K231(b₁ : ( ( ) ( ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool b₁ : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) SetSequence of Sigma : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) SigmaField of b₁ : ( ( ) ( ) set ) ) )
for B being ( ( ) ( ) Event of Sigma : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) SigmaField of b₁ : ( ( ) ( ) set ) ) ) st ( for n being ( ( ) ( ext-real epsilon-transitive epsilon-connected ordinal natural V14() real V33() V34() V45() V46() V47() V48() V49() V50() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) ) holds BSeq : ( ( b₂ : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) SigmaField of b₁ : ( ( ) ( ) set ) ) -valued Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) ,K231(b₁ : ( ( ) ( ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool b₁ : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) -defined b₂ : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) SigmaField of b₁ : ( ( ) ( ) set ) ) -valued K231(b₁ : ( ( ) ( ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool b₁ : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) ,K231(b₁ : ( ( ) ( ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool b₁ : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) SetSequence of b₂ : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) SigmaField of b₁ : ( ( ) ( ) set ) ) ) . n : ( ( ) ( ext-real epsilon-transitive epsilon-connected ordinal natural V14() real V33() V34() V45() V46() V47() V48() V49() V50() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Event of b₂ : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) SigmaField of b₁ : ( ( ) ( ) set ) ) ) = (ASeq : ( ( b₂ : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) SigmaField of b₁ : ( ( ) ( ) set ) ) -valued Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) ,K231(b₁ : ( ( ) ( ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool b₁ : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) -defined b₂ : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) SigmaField of b₁ : ( ( ) ( ) set ) ) -valued K231(b₁ : ( ( ) ( ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool b₁ : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) ,K231(b₁ : ( ( ) ( ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool b₁ : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) SetSequence of b₂ : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) SigmaField of b₁ : ( ( ) ( ) set ) ) ) . n : ( ( ) ( ext-real epsilon-transitive epsilon-connected ordinal natural V14() real V33() V34() V45() V46() V47() V48() V49() V50() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( ) Event of b₂ : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) SigmaField of b₁ : ( ( ) ( ) set ) ) ) /\ B : ( ( ) ( ) Event of b₂ : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) SigmaField of b₁ : ( ( ) ( ) set ) ) ) : ( ( ) ( ) Event of b₂ : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) SigmaField of b₁ : ( ( ) ( ) set ) ) ) ) holds
(Intersection ASeq : ( ( b₂ : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) SigmaField of b₁ : ( ( ) ( ) set ) ) -valued Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) ,K231(b₁ : ( ( ) ( ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool b₁ : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) -defined b₂ : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) SigmaField of b₁ : ( ( ) ( ) set ) ) -valued K231(b₁ : ( ( ) ( ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool b₁ : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) ,K231(b₁ : ( ( ) ( ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool b₁ : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) SetSequence of b₂ : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) SigmaField of b₁ : ( ( ) ( ) set ) ) ) ) : ( ( ) ( ) Element of bool b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) /\ B : ( ( ) ( ) Event of b₂ : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) SigmaField of b₁ : ( ( ) ( ) set ) ) ) : ( ( ) ( ) Element of bool b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) = Intersection BSeq : ( ( b₂ : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) SigmaField of b₁ : ( ( ) ( ) set ) ) -valued Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) ,K231(b₁ : ( ( ) ( ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool b₁ : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) -defined b₂ : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) SigmaField of b₁ : ( ( ) ( ) set ) ) -valued K231(b₁ : ( ( ) ( ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool b₁ : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) ,K231(b₁ : ( ( ) ( ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool b₁ : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) SetSequence of b₂ : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) SigmaField of b₁ : ( ( ) ( ) set ) ) ) : ( ( ) ( ) Element of bool b₁ : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ;

registration

cluster Complement ASeq : ( ( Sigma : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) ,K231(Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) -defined Sigma : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued K231(Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) ,K231(Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) Element of bool [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) ,K231(Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) : ( ( Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) ,K231(Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) -defined K231(Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) ,K231(Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) Element of bool [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) ,K231(Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -> Sigma : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) ,K231(Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ;

end;

theorem :: PROB_2:6

for X being ( ( ) ( ) set )
for S being ( ( Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) ,K231(b₁ : ( ( ) ( ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool b₁ : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) -defined K231(b₁ : ( ( ) ( ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool b₁ : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) ,K231(b₁ : ( ( ) ( ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool b₁ : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) SetSequence of ( ( ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool X : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) holds
( S : ( ( Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) ,K231(b₁ : ( ( ) ( ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool b₁ : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) -defined K231(b₁ : ( ( ) ( ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool b₁ : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) ,K231(b₁ : ( ( ) ( ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool b₁ : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) SetSequence of ( ( ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool b₁ : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) is non-ascending iff for n being ( ( ) ( ext-real epsilon-transitive epsilon-connected ordinal natural V14() real V33() V34() V45() V46() V47() V48() V49() V50() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) ) holds S : ( ( Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) ,K231(b₁ : ( ( ) ( ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool b₁ : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) -defined K231(b₁ : ( ( ) ( ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool b₁ : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) ,K231(b₁ : ( ( ) ( ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool b₁ : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) SetSequence of ( ( ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool b₁ : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) . (n : ( ( ) ( ext-real epsilon-transitive epsilon-connected ordinal natural V14() real V33() V34() V45() V46() V47() V48() V49() V50() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) ) + 1 : ( ( ) ( ext-real positive non negative non empty epsilon-transitive epsilon-connected ordinal natural V14() real V33() V34() V45() V46() V47() V48() V49() V50() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( ext-real epsilon-transitive epsilon-connected ordinal natural V14() real V33() V34() V45() V46() V47() V48() V49() V50() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Event of K231(b₁ : ( ( ) ( ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool b₁ : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) c= S : ( ( Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) ,K231(b₁ : ( ( ) ( ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool b₁ : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) -defined K231(b₁ : ( ( ) ( ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool b₁ : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) ,K231(b₁ : ( ( ) ( ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool b₁ : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) SetSequence of ( ( ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool b₁ : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) . n : ( ( ) ( ext-real epsilon-transitive epsilon-connected ordinal natural V14() real V33() V34() V45() V46() V47() V48() V49() V50() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Event of K231(b₁ : ( ( ) ( ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool b₁ : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) ;

theorem :: PROB_2:7

for X being ( ( ) ( ) set )
for S being ( ( Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) ,K231(b₁ : ( ( ) ( ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool b₁ : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) -defined K231(b₁ : ( ( ) ( ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool b₁ : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) ,K231(b₁ : ( ( ) ( ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool b₁ : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) SetSequence of ( ( ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool X : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) holds
( S : ( ( Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) ,K231(b₁ : ( ( ) ( ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool b₁ : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) -defined K231(b₁ : ( ( ) ( ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool b₁ : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) ,K231(b₁ : ( ( ) ( ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool b₁ : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) SetSequence of ( ( ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool b₁ : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) is non-descending iff for n being ( ( ) ( ext-real epsilon-transitive epsilon-connected ordinal natural V14() real V33() V34() V45() V46() V47() V48() V49() V50() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) ) holds S : ( ( Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) ,K231(b₁ : ( ( ) ( ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool b₁ : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) -defined K231(b₁ : ( ( ) ( ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool b₁ : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) ,K231(b₁ : ( ( ) ( ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool b₁ : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) SetSequence of ( ( ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool b₁ : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) . n : ( ( ) ( ext-real epsilon-transitive epsilon-connected ordinal natural V14() real V33() V34() V45() V46() V47() V48() V49() V50() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Event of K231(b₁ : ( ( ) ( ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool b₁ : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) c= S : ( ( Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) ,K231(b₁ : ( ( ) ( ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool b₁ : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) -defined K231(b₁ : ( ( ) ( ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool b₁ : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) ,K231(b₁ : ( ( ) ( ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool b₁ : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) SetSequence of ( ( ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool b₁ : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) . (n : ( ( ) ( ext-real epsilon-transitive epsilon-connected ordinal natural V14() real V33() V34() V45() V46() V47() V48() V49() V50() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) ) + 1 : ( ( ) ( ext-real positive non negative non empty epsilon-transitive epsilon-connected ordinal natural V14() real V33() V34() V45() V46() V47() V48() V49() V50() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( ext-real epsilon-transitive epsilon-connected ordinal natural V14() real V33() V34() V45() V46() V47() V48() V49() V50() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Event of K231(b₁ : ( ( ) ( ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool b₁ : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) ;

theorem :: PROB_2:8

for Omega being ( ( ) ( ) set )
for ASeq being ( ( Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) ,K231(b₁ : ( ( ) ( ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool b₁ : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) -defined K231(b₁ : ( ( ) ( ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool b₁ : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) ,K231(b₁ : ( ( ) ( ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool b₁ : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) SetSequence of ( ( ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) holds
( ASeq : ( ( Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) ,K231(b₁ : ( ( ) ( ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool b₁ : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) -defined K231(b₁ : ( ( ) ( ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool b₁ : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) ,K231(b₁ : ( ( ) ( ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool b₁ : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) SetSequence of ( ( ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool b₁ : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) is non-ascending iff Complement ASeq : ( ( Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) ,K231(b₁ : ( ( ) ( ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool b₁ : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) -defined K231(b₁ : ( ( ) ( ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool b₁ : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) ,K231(b₁ : ( ( ) ( ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool b₁ : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) SetSequence of ( ( ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool b₁ : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) ,K231(b₁ : ( ( ) ( ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool b₁ : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) -defined K231(b₁ : ( ( ) ( ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool b₁ : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued K231(b₁ : ( ( ) ( ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool b₁ : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) ,K231(b₁ : ( ( ) ( ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool b₁ : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) Element of bool [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) ,K231(b₁ : ( ( ) ( ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool b₁ : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) is non-descending ) ;

definition

let F be ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) ;

attr F is disjoint_valued means :: PROB_2:def 2
for x, y being ( ( ) ( ) set ) st x : ( ( ) ( ) set ) <> y : ( ( ) ( ) set ) holds
F : ( ( ) ( ) set ) . x : ( ( ) ( ) set ) : ( ( ) ( ) set ) misses F : ( ( ) ( ) set ) . y : ( ( ) ( ) set ) : ( ( ) ( ) set ) ;

end;

definition

:: original: disjoint_valued
redefine attr ASeq is disjoint_valued means :: PROB_2:def 3
for m, n being ( ( ) ( ext-real epsilon-transitive epsilon-connected ordinal natural V14() real V33() V34() V45() V46() V47() V48() V49() V50() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) ) st m : ( ( ) ( ext-real epsilon-transitive epsilon-connected ordinal natural V14() real V33() V34() V45() V46() V47() V48() V49() V50() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) ) <> n : ( ( ) ( ext-real epsilon-transitive epsilon-connected ordinal natural V14() real V33() V34() V45() V46() V47() V48() V49() V50() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) ) holds
ASeq : ( ( Sigma : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) ,K231(Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) -defined Sigma : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued K231(Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) ,K231(Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) Element of bool [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) ,K231(Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) . m : ( ( ) ( ext-real epsilon-transitive epsilon-connected ordinal natural V14() real V33() V34() V45() V46() V47() V48() V49() V50() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Event of Sigma : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) misses ASeq : ( ( Sigma : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) ,K231(Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) -defined Sigma : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued K231(Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) ,K231(Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) Element of bool [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) ,K231(Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) . n : ( ( ) ( ext-real epsilon-transitive epsilon-connected ordinal natural V14() real V33() V34() V45() V46() V47() V48() V49() V50() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Event of Sigma : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ;

end;

theorem :: PROB_2:9

theorem :: PROB_2:10

theorem :: PROB_2:11

theorem :: PROB_2:12

theorem :: PROB_2:13

theorem :: PROB_2:14

theorem :: PROB_2:15

theorem :: PROB_2:16

theorem :: PROB_2:17

theorem :: PROB_2:18

definition

pred A,B are_independent_respect_to P means :: PROB_2:def 4
P : ( ( Sigma : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) ,K231(Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) -defined Sigma : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued K231(Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) ,K231(Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) Element of bool [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) ,K231(Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) . (A : ( ( ) ( ) set ) /\ B : ( ( ) ( ) set ) ) : ( ( ) ( ) Event of Sigma : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ext-real V14() real ) Element of REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) = (P : ( ( Sigma : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) ,K231(Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) -defined Sigma : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued K231(Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) ,K231(Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) Element of bool [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) ,K231(Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) . A : ( ( ) ( ) set ) ) : ( ( ) ( ext-real V14() real ) Element of REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) * (P : ( ( Sigma : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) ,K231(Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) -defined Sigma : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued K231(Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) ,K231(Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) Element of bool [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) ,K231(Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) . B : ( ( ) ( ) set ) ) : ( ( ) ( ext-real V14() real ) Element of REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ext-real V14() real ) Element of REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) ;

let C be ( ( ) ( ) Event of Sigma : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) SigmaField of Omega : ( ( non empty ) ( non empty ) set ) ) ) ;

pred A,B,C are_independent_respect_to P means :: PROB_2:def 5
( P : ( ( Sigma : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) ,K231(Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) -defined Sigma : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued K231(Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) ,K231(Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) Element of bool [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) ,K231(Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) . ((A : ( ( ) ( ) set ) /\ B : ( ( ) ( ) set ) ) : ( ( ) ( ) Event of Sigma : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) /\ C : ( ( Function-like V30(P : ( ( Sigma : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) ,K231(Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) -defined Sigma : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued K231(Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) ,K231(Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) Element of bool [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) ,K231(Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ,A : ( ( ) ( ) set ) ) ) ( Relation-like P : ( ( Sigma : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) ,K231(Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) -defined Sigma : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued K231(Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) ,K231(Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) Element of bool [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) ,K231(Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -defined A : ( ( ) ( ) set ) -valued Function-like V30(P : ( ( Sigma : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) ,K231(Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) -defined Sigma : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued K231(Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) ,K231(Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) Element of bool [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) ,K231(Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ,A : ( ( ) ( ) set ) ) ) Element of bool [:P : ( ( Sigma : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) ,K231(Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) -defined Sigma : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued K231(Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) ,K231(Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) Element of bool [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) ,K231(Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ,A : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Event of Sigma : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ext-real V14() real ) Element of REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) = ((P : ( ( Sigma : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) ,K231(Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) -defined Sigma : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued K231(Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) ,K231(Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) Element of bool [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) ,K231(Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) . A : ( ( ) ( ) set ) ) : ( ( ) ( ext-real V14() real ) Element of REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) * (P : ( ( Sigma : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) ,K231(Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) -defined Sigma : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued K231(Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) ,K231(Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) Element of bool [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) ,K231(Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) . B : ( ( ) ( ) set ) ) : ( ( ) ( ext-real V14() real ) Element of REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) ) : ( ( ) ( ext-real V14() real ) Element of REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) * (P : ( ( Sigma : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) ,K231(Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) -defined Sigma : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued K231(Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) ,K231(Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) Element of bool [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) ,K231(Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) . C : ( ( Function-like V30(P : ( ( Sigma : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) ,K231(Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) -defined Sigma : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued K231(Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) ,K231(Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) Element of bool [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) ,K231(Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ,A : ( ( ) ( ) set ) ) ) ( Relation-like P : ( ( Sigma : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) ,K231(Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) -defined Sigma : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued K231(Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) ,K231(Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) Element of bool [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) ,K231(Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -defined A : ( ( ) ( ) set ) -valued Function-like V30(P : ( ( Sigma : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) ,K231(Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) -defined Sigma : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued K231(Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) ,K231(Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) Element of bool [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) ,K231(Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ,A : ( ( ) ( ) set ) ) ) Element of bool [:P : ( ( Sigma : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) ,K231(Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) -defined Sigma : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued K231(Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) ,K231(Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) Element of bool [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) ,K231(Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ,A : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ext-real V14() real ) Element of REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ext-real V14() real ) Element of REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) & P : ( ( Sigma : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) ,K231(Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) -defined Sigma : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued K231(Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) ,K231(Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) Element of bool [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) ,K231(Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) . (A : ( ( ) ( ) set ) /\ B : ( ( ) ( ) set ) ) : ( ( ) ( ) Event of Sigma : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ext-real V14() real ) Element of REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) = (P : ( ( Sigma : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) ,K231(Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) -defined Sigma : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued K231(Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) ,K231(Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) Element of bool [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) ,K231(Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) . A : ( ( ) ( ) set ) ) : ( ( ) ( ext-real V14() real ) Element of REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) * (P : ( ( Sigma : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) ,K231(Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) -defined Sigma : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued K231(Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) ,K231(Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) Element of bool [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) ,K231(Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) . B : ( ( ) ( ) set ) ) : ( ( ) ( ext-real V14() real ) Element of REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ext-real V14() real ) Element of REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) & P : ( ( Sigma : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) ,K231(Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) -defined Sigma : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued K231(Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) ,K231(Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) Element of bool [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) ,K231(Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) . (A : ( ( ) ( ) set ) /\ C : ( ( Function-like V30(P : ( ( Sigma : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) ,K231(Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) -defined Sigma : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued K231(Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) ,K231(Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) Element of bool [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) ,K231(Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ,A : ( ( ) ( ) set ) ) ) ( Relation-like P : ( ( Sigma : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) ,K231(Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) -defined Sigma : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued K231(Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) ,K231(Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) Element of bool [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) ,K231(Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -defined A : ( ( ) ( ) set ) -valued Function-like V30(P : ( ( Sigma : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) ,K231(Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) -defined Sigma : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued K231(Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) ,K231(Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) Element of bool [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) ,K231(Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ,A : ( ( ) ( ) set ) ) ) Element of bool [:P : ( ( Sigma : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) ,K231(Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) -defined Sigma : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued K231(Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) ,K231(Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) Element of bool [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) ,K231(Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ,A : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Event of Sigma : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ext-real V14() real ) Element of REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) = (P : ( ( Sigma : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) ,K231(Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) -defined Sigma : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued K231(Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) ,K231(Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) Element of bool [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) ,K231(Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) . A : ( ( ) ( ) set ) ) : ( ( ) ( ext-real V14() real ) Element of REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) * (P : ( ( Sigma : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) ,K231(Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) -defined Sigma : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued K231(Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) ,K231(Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) Element of bool [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) ,K231(Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) . C : ( ( Function-like V30(P : ( ( Sigma : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) ,K231(Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) -defined Sigma : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued K231(Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) ,K231(Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) Element of bool [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) ,K231(Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ,A : ( ( ) ( ) set ) ) ) ( Relation-like P : ( ( Sigma : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) ,K231(Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) -defined Sigma : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued K231(Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) ,K231(Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) Element of bool [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) ,K231(Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -defined A : ( ( ) ( ) set ) -valued Function-like V30(P : ( ( Sigma : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) ,K231(Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) -defined Sigma : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued K231(Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) ,K231(Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) Element of bool [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) ,K231(Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ,A : ( ( ) ( ) set ) ) ) Element of bool [:P : ( ( Sigma : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) ,K231(Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) -defined Sigma : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued K231(Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) ,K231(Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) Element of bool [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) ,K231(Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ,A : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ext-real V14() real ) Element of REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ext-real V14() real ) Element of REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) & P : ( ( Sigma : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) ,K231(Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) -defined Sigma : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued K231(Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) ,K231(Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) Element of bool [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) ,K231(Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) . (B : ( ( ) ( ) set ) /\ C : ( ( Function-like V30(P : ( ( Sigma : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) ,K231(Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) -defined Sigma : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued K231(Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) ,K231(Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) Element of bool [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) ,K231(Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ,A : ( ( ) ( ) set ) ) ) ( Relation-like P : ( ( Sigma : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) ,K231(Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) -defined Sigma : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued K231(Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) ,K231(Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) Element of bool [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) ,K231(Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -defined A : ( ( ) ( ) set ) -valued Function-like V30(P : ( ( Sigma : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) ,K231(Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) -defined Sigma : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued K231(Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) ,K231(Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) Element of bool [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) ,K231(Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ,A : ( ( ) ( ) set ) ) ) Element of bool [:P : ( ( Sigma : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) ,K231(Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) -defined Sigma : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued K231(Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) ,K231(Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) Element of bool [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) ,K231(Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ,A : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Event of Sigma : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ext-real V14() real ) Element of REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) = (P : ( ( Sigma : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) ,K231(Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) -defined Sigma : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued K231(Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) ,K231(Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) Element of bool [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) ,K231(Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) . B : ( ( ) ( ) set ) ) : ( ( ) ( ext-real V14() real ) Element of REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) * (P : ( ( Sigma : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) ,K231(Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) -defined Sigma : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued K231(Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) ,K231(Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) Element of bool [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) ,K231(Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) . C : ( ( Function-like V30(P : ( ( Sigma : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) ,K231(Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) -defined Sigma : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued K231(Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) ,K231(Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) Element of bool [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) ,K231(Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ,A : ( ( ) ( ) set ) ) ) ( Relation-like P : ( ( Sigma : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) ,K231(Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) -defined Sigma : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued K231(Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) ,K231(Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) Element of bool [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) ,K231(Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -defined A : ( ( ) ( ) set ) -valued Function-like V30(P : ( ( Sigma : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) ,K231(Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) -defined Sigma : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued K231(Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) ,K231(Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) Element of bool [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) ,K231(Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ,A : ( ( ) ( ) set ) ) ) Element of bool [:P : ( ( Sigma : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) ,K231(Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) -defined Sigma : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued K231(Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) ,K231(Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) Element of bool [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) ,K231(Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ,A : ( ( ) ( ) set ) :] : ( ( ) ( ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ext-real V14() real ) Element of REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ext-real V14() real ) Element of REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) );

end;

theorem :: PROB_2:19

theorem :: PROB_2:20

theorem :: PROB_2:21

theorem :: PROB_2:22

theorem :: PROB_2:23

theorem :: PROB_2:24

theorem :: PROB_2:25

theorem :: PROB_2:26

theorem :: PROB_2:27

theorem :: PROB_2:28

definition

let Omega be ( ( non empty ) ( non empty ) set ) ;
let Sigma be ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) SigmaField of Omega : ( ( non empty ) ( non empty ) set ) ) ;
let P be ( ( ) ( Relation-like Sigma : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) SigmaField of Omega : ( ( non empty ) ( non empty ) set ) ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) -valued Function-like V30(Sigma : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) SigmaField of Omega : ( ( non empty ) ( non empty ) set ) ) , REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) V35() V36() V37() V44() ) Probability of Sigma : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) SigmaField of Omega : ( ( non empty ) ( non empty ) set ) ) ) ;
let B be ( ( ) ( ) Event of Sigma : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) SigmaField of Omega : ( ( non empty ) ( non empty ) set ) ) ) ;
assume 0 : ( ( ) ( ext-real non positive non negative empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V14() real V33() V34() V45() V46() V47() V48() V49() V50() V51() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) ) < P : ( ( ) ( Relation-like Sigma : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) SigmaField of Omega : ( ( non empty ) ( non empty ) set ) ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) -valued Function-like V30(Sigma : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) SigmaField of Omega : ( ( non empty ) ( non empty ) set ) ) , REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) V35() V36() V37() V44() ) Probability of Sigma : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) SigmaField of Omega : ( ( non empty ) ( non empty ) set ) ) ) . B : ( ( ) ( ) Event of Sigma : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) SigmaField of Omega : ( ( non empty ) ( non empty ) set ) ) ) : ( ( ) ( ext-real V14() real ) Element of REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) ;

func P .|. B -> ( ( ) ( Relation-like Sigma : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) -valued Function-like V30(Sigma : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) , REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) V35() V36() V37() V44() ) Probability of Sigma : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) means :: PROB_2:def 6
for A being ( ( ) ( ) Event of Sigma : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) holds it : ( ( ) ( ) set ) . A : ( ( ) ( ) Event of Sigma : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) SigmaField of Omega : ( ( non empty ) ( non empty ) set ) ) ) : ( ( ) ( ext-real V14() real ) Element of REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) = (P : ( ( Sigma : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) ,K231(Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) -defined Sigma : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued K231(Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) ,K231(Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) Element of bool [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) ,K231(Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) . (A : ( ( ) ( ) Event of Sigma : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) SigmaField of Omega : ( ( non empty ) ( non empty ) set ) ) ) /\ B : ( ( ) ( ) set ) ) : ( ( ) ( ) Event of Sigma : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( ext-real V14() real ) Element of REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) / (P : ( ( Sigma : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) ,K231(Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) ( Relation-like NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) -defined Sigma : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued K231(Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) -valued Function-like V30( NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) ,K231(Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) ) Element of bool [:NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) ,K231(Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty compl-closed sigma-multiplicative ) Element of bool (bool Omega : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) :] : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) . B : ( ( ) ( ) set ) ) : ( ( ) ( ext-real V14() real ) Element of REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ext-real V14() real ) Element of REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) ;

end;

theorem :: PROB_2:29

theorem :: PROB_2:30

theorem :: PROB_2:31

theorem :: PROB_2:32

theorem :: PROB_2:33

theorem :: PROB_2:34

theorem :: PROB_2:35

theorem :: PROB_2:36

theorem :: PROB_2:37

theorem :: PROB_2:38

for Omega being ( ( non empty ) ( non empty ) set )
for Sigma being ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) SigmaField of Omega : ( ( non empty ) ( non empty ) set ) )
for B, A1, A2, A3 being ( ( ) ( ) Event of Sigma : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) SigmaField of b₁ : ( ( non empty ) ( non empty ) set ) ) )
for P being ( ( ) ( Relation-like b₂ : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) SigmaField of b₁ : ( ( non empty ) ( non empty ) set ) ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) -valued Function-like V30(b₂ : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) SigmaField of b₁ : ( ( non empty ) ( non empty ) set ) ) , REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) V35() V36() V37() V44() ) Probability of Sigma : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) SigmaField of b₁ : ( ( non empty ) ( non empty ) set ) ) ) st 0 : ( ( ) ( ext-real non positive non negative empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V14() real V33() V34() V45() V46() V47() V48() V49() V50() V51() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) ) < P : ( ( ) ( Relation-like b₂ : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) SigmaField of b₁ : ( ( non empty ) ( non empty ) set ) ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) -valued Function-like V30(b₂ : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) SigmaField of b₁ : ( ( non empty ) ( non empty ) set ) ) , REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) V35() V36() V37() V44() ) Probability of b₂ : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) SigmaField of b₁ : ( ( non empty ) ( non empty ) set ) ) ) . B : ( ( ) ( ) Event of b₂ : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) SigmaField of b₁ : ( ( non empty ) ( non empty ) set ) ) ) : ( ( ) ( ext-real V14() real ) Element of REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) & 0 : ( ( ) ( ext-real non positive non negative empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V14() real V33() V34() V45() V46() V47() V48() V49() V50() V51() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) ) < P : ( ( ) ( Relation-like b₂ : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) SigmaField of b₁ : ( ( non empty ) ( non empty ) set ) ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) -valued Function-like V30(b₂ : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) SigmaField of b₁ : ( ( non empty ) ( non empty ) set ) ) , REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) V35() V36() V37() V44() ) Probability of b₂ : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) SigmaField of b₁ : ( ( non empty ) ( non empty ) set ) ) ) . A1 : ( ( ) ( ) Event of b₂ : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) SigmaField of b₁ : ( ( non empty ) ( non empty ) set ) ) ) : ( ( ) ( ext-real V14() real ) Element of REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) & 0 : ( ( ) ( ext-real non positive non negative empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V14() real V33() V34() V45() V46() V47() V48() V49() V50() V51() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) ) < P : ( ( ) ( Relation-like b₂ : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) SigmaField of b₁ : ( ( non empty ) ( non empty ) set ) ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) -valued Function-like V30(b₂ : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) SigmaField of b₁ : ( ( non empty ) ( non empty ) set ) ) , REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) V35() V36() V37() V44() ) Probability of b₂ : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) SigmaField of b₁ : ( ( non empty ) ( non empty ) set ) ) ) . A2 : ( ( ) ( ) Event of b₂ : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) SigmaField of b₁ : ( ( non empty ) ( non empty ) set ) ) ) : ( ( ) ( ext-real V14() real ) Element of REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) & 0 : ( ( ) ( ext-real non positive non negative empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V14() real V33() V34() V45() V46() V47() V48() V49() V50() V51() ) Element of NAT : ( ( ) ( non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() ) Element of bool REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) : ( ( ) ( non empty ) set ) ) ) < P : ( ( ) ( Relation-like b₂ : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) SigmaField of b₁ : ( ( non empty ) ( non empty ) set ) ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) -valued Function-like V30(b₂ : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) SigmaField of b₁ : ( ( non empty ) ( non empty ) set ) ) , REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) V35() V36() V37() V44() ) Probability of b₂ : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) SigmaField of b₁ : ( ( non empty ) ( non empty ) set ) ) ) . A3 : ( ( ) ( ) Event of b₂ : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) SigmaField of b₁ : ( ( non empty ) ( non empty ) set ) ) ) : ( ( ) ( ext-real V14() real ) Element of REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) & A1 : ( ( ) ( ) Event of b₂ : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) SigmaField of b₁ : ( ( non empty ) ( non empty ) set ) ) ) misses A2 : ( ( ) ( ) Event of b₂ : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) SigmaField of b₁ : ( ( non empty ) ( non empty ) set ) ) ) & A3 : ( ( ) ( ) Event of b₂ : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) SigmaField of b₁ : ( ( non empty ) ( non empty ) set ) ) ) = (A1 : ( ( ) ( ) Event of b₂ : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) SigmaField of b₁ : ( ( non empty ) ( non empty ) set ) ) ) \/ A2 : ( ( ) ( ) Event of b₂ : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) SigmaField of b₁ : ( ( non empty ) ( non empty ) set ) ) ) ) : ( ( ) ( ) Event of b₂ : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) SigmaField of b₁ : ( ( non empty ) ( non empty ) set ) ) ) ` : ( ( ) ( ) Element of bool b₁ : ( ( non empty ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) holds
( (P : ( ( ) ( Relation-like b₂ : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) SigmaField of b₁ : ( ( non empty ) ( non empty ) set ) ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) -valued Function-like V30(b₂ : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) SigmaField of b₁ : ( ( non empty ) ( non empty ) set ) ) , REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) V35() V36() V37() V44() ) Probability of b₂ : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) SigmaField of b₁ : ( ( non empty ) ( non empty ) set ) ) ) .|. B : ( ( ) ( ) Event of b₂ : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) SigmaField of b₁ : ( ( non empty ) ( non empty ) set ) ) ) ) : ( ( ) ( Relation-like b₂ : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) SigmaField of b₁ : ( ( non empty ) ( non empty ) set ) ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) -valued Function-like V30(b₂ : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) SigmaField of b₁ : ( ( non empty ) ( non empty ) set ) ) , REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) V35() V36() V37() V44() ) Probability of b₂ : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) SigmaField of b₁ : ( ( non empty ) ( non empty ) set ) ) ) . A1 : ( ( ) ( ) Event of b₂ : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) SigmaField of b₁ : ( ( non empty ) ( non empty ) set ) ) ) : ( ( ) ( ext-real V14() real ) Element of REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) = (((P : ( ( ) ( Relation-like b₂ : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) SigmaField of b₁ : ( ( non empty ) ( non empty ) set ) ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) -valued Function-like V30(b₂ : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) SigmaField of b₁ : ( ( non empty ) ( non empty ) set ) ) , REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) V35() V36() V37() V44() ) Probability of b₂ : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) SigmaField of b₁ : ( ( non empty ) ( non empty ) set ) ) ) .|. A1 : ( ( ) ( ) Event of b₂ : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) SigmaField of b₁ : ( ( non empty ) ( non empty ) set ) ) ) ) : ( ( ) ( Relation-like b₂ : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) SigmaField of b₁ : ( ( non empty ) ( non empty ) set ) ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) -valued Function-like V30(b₂ : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) SigmaField of b₁ : ( ( non empty ) ( non empty ) set ) ) , REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) V35() V36() V37() V44() ) Probability of b₂ : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) SigmaField of b₁ : ( ( non empty ) ( non empty ) set ) ) ) . B : ( ( ) ( ) Event of b₂ : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) SigmaField of b₁ : ( ( non empty ) ( non empty ) set ) ) ) ) : ( ( ) ( ext-real V14() real ) Element of REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) * (P : ( ( ) ( Relation-like b₂ : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) SigmaField of b₁ : ( ( non empty ) ( non empty ) set ) ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) -valued Function-like V30(b₂ : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) SigmaField of b₁ : ( ( non empty ) ( non empty ) set ) ) , REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) V35() V36() V37() V44() ) Probability of b₂ : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) SigmaField of b₁ : ( ( non empty ) ( non empty ) set ) ) ) . A1 : ( ( ) ( ) Event of b₂ : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) SigmaField of b₁ : ( ( non empty ) ( non empty ) set ) ) ) ) : ( ( ) ( ext-real V14() real ) Element of REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) ) : ( ( ) ( ext-real V14() real ) Element of REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) / (((((P : ( ( ) ( Relation-like b₂ : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) SigmaField of b₁ : ( ( non empty ) ( non empty ) set ) ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) -valued Function-like V30(b₂ : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) SigmaField of b₁ : ( ( non empty ) ( non empty ) set ) ) , REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) V35() V36() V37() V44() ) Probability of b₂ : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) SigmaField of b₁ : ( ( non empty ) ( non empty ) set ) ) ) .|. A1 : ( ( ) ( ) Event of b₂ : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) SigmaField of b₁ : ( ( non empty ) ( non empty ) set ) ) ) ) : ( ( ) ( Relation-like b₂ : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) SigmaField of b₁ : ( ( non empty ) ( non empty ) set ) ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) -valued Function-like V30(b₂ : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) SigmaField of b₁ : ( ( non empty ) ( non empty ) set ) ) , REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) V35() V36() V37() V44() ) Probability of b₂ : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) SigmaField of b₁ : ( ( non empty ) ( non empty ) set ) ) ) . B : ( ( ) ( ) Event of b₂ : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) SigmaField of b₁ : ( ( non empty ) ( non empty ) set ) ) ) ) : ( ( ) ( ext-real V14() real ) Element of REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) * (P : ( ( ) ( Relation-like b₂ : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) SigmaField of b₁ : ( ( non empty ) ( non empty ) set ) ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) -valued Function-like V30(b₂ : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) SigmaField of b₁ : ( ( non empty ) ( non empty ) set ) ) , REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) V35() V36() V37() V44() ) Probability of b₂ : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) SigmaField of b₁ : ( ( non empty ) ( non empty ) set ) ) ) . A1 : ( ( ) ( ) Event of b₂ : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) SigmaField of b₁ : ( ( non empty ) ( non empty ) set ) ) ) ) : ( ( ) ( ext-real V14() real ) Element of REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) ) : ( ( ) ( ext-real V14() real ) Element of REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) + (((P : ( ( ) ( Relation-like b₂ : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) SigmaField of b₁ : ( ( non empty ) ( non empty ) set ) ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) -valued Function-like V30(b₂ : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) SigmaField of b₁ : ( ( non empty ) ( non empty ) set ) ) , REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) V35() V36() V37() V44() ) Probability of b₂ : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) SigmaField of b₁ : ( ( non empty ) ( non empty ) set ) ) ) .|. A2 : ( ( ) ( ) Event of b₂ : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) SigmaField of b₁ : ( ( non empty ) ( non empty ) set ) ) ) ) : ( ( ) ( Relation-like b₂ : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) SigmaField of b₁ : ( ( non empty ) ( non empty ) set ) ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) -valued Function-like V30(b₂ : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) SigmaField of b₁ : ( ( non empty ) ( non empty ) set ) ) , REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) V35() V36() V37() V44() ) Probability of b₂ : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) SigmaField of b₁ : ( ( non empty ) ( non empty ) set ) ) ) . B : ( ( ) ( ) Event of b₂ : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) SigmaField of b₁ : ( ( non empty ) ( non empty ) set ) ) ) ) : ( ( ) ( ext-real V14() real ) Element of REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) * (P : ( ( ) ( Relation-like b₂ : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) SigmaField of b₁ : ( ( non empty ) ( non empty ) set ) ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) -valued Function-like V30(b₂ : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) SigmaField of b₁ : ( ( non empty ) ( non empty ) set ) ) , REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) V35() V36() V37() V44() ) Probability of b₂ : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) SigmaField of b₁ : ( ( non empty ) ( non empty ) set ) ) ) . A2 : ( ( ) ( ) Event of b₂ : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) SigmaField of b₁ : ( ( non empty ) ( non empty ) set ) ) ) ) : ( ( ) ( ext-real V14() real ) Element of REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) ) : ( ( ) ( ext-real V14() real ) Element of REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) ) : ( ( ) ( ext-real V14() real ) Element of REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) + (((P : ( ( ) ( Relation-like b₂ : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) SigmaField of b₁ : ( ( non empty ) ( non empty ) set ) ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) -valued Function-like V30(b₂ : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) SigmaField of b₁ : ( ( non empty ) ( non empty ) set ) ) , REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) V35() V36() V37() V44() ) Probability of b₂ : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) SigmaField of b₁ : ( ( non empty ) ( non empty ) set ) ) ) .|. A3 : ( ( ) ( ) Event of b₂ : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) SigmaField of b₁ : ( ( non empty ) ( non empty ) set ) ) ) ) : ( ( ) ( Relation-like b₂ : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) SigmaField of b₁ : ( ( non empty ) ( non empty ) set ) ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) -valued Function-like V30(b₂ : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) SigmaField of b₁ : ( ( non empty ) ( non empty ) set ) ) , REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) V35() V36() V37() V44() ) Probability of b₂ : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) SigmaField of b₁ : ( ( non empty ) ( non empty ) set ) ) ) . B : ( ( ) ( ) Event of b₂ : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) SigmaField of b₁ : ( ( non empty ) ( non empty ) set ) ) ) ) : ( ( ) ( ext-real V14() real ) Element of REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) * (P : ( ( ) ( Relation-like b₂ : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) SigmaField of b₁ : ( ( non empty ) ( non empty ) set ) ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) -valued Function-like V30(b₂ : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) SigmaField of b₁ : ( ( non empty ) ( non empty ) set ) ) , REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) V35() V36() V37() V44() ) Probability of b₂ : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) SigmaField of b₁ : ( ( non empty ) ( non empty ) set ) ) ) . A3 : ( ( ) ( ) Event of b₂ : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) SigmaField of b₁ : ( ( non empty ) ( non empty ) set ) ) ) ) : ( ( ) ( ext-real V14() real ) Element of REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) ) : ( ( ) ( ext-real V14() real ) Element of REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) ) : ( ( ) ( ext-real V14() real ) Element of REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ext-real V14() real ) Element of REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) & (P : ( ( ) ( Relation-like b₂ : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) SigmaField of b₁ : ( ( non empty ) ( non empty ) set ) ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) -valued Function-like V30(b₂ : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) SigmaField of b₁ : ( ( non empty ) ( non empty ) set ) ) , REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) V35() V36() V37() V44() ) Probability of b₂ : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) SigmaField of b₁ : ( ( non empty ) ( non empty ) set ) ) ) .|. B : ( ( ) ( ) Event of b₂ : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) SigmaField of b₁ : ( ( non empty ) ( non empty ) set ) ) ) ) : ( ( ) ( Relation-like b₂ : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) SigmaField of b₁ : ( ( non empty ) ( non empty ) set ) ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) -valued Function-like V30(b₂ : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) SigmaField of b₁ : ( ( non empty ) ( non empty ) set ) ) , REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) V35() V36() V37() V44() ) Probability of b₂ : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) SigmaField of b₁ : ( ( non empty ) ( non empty ) set ) ) ) . A2 : ( ( ) ( ) Event of b₂ : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) SigmaField of b₁ : ( ( non empty ) ( non empty ) set ) ) ) : ( ( ) ( ext-real V14() real ) Element of REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) = (((P : ( ( ) ( Relation-like b₂ : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) SigmaField of b₁ : ( ( non empty ) ( non empty ) set ) ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) -valued Function-like V30(b₂ : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) SigmaField of b₁ : ( ( non empty ) ( non empty ) set ) ) , REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) V35() V36() V37() V44() ) Probability of b₂ : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) SigmaField of b₁ : ( ( non empty ) ( non empty ) set ) ) ) .|. A2 : ( ( ) ( ) Event of b₂ : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) SigmaField of b₁ : ( ( non empty ) ( non empty ) set ) ) ) ) : ( ( ) ( Relation-like b₂ : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) SigmaField of b₁ : ( ( non empty ) ( non empty ) set ) ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) -valued Function-like V30(b₂ : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) SigmaField of b₁ : ( ( non empty ) ( non empty ) set ) ) , REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) V35() V36() V37() V44() ) Probability of b₂ : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) SigmaField of b₁ : ( ( non empty ) ( non empty ) set ) ) ) . B : ( ( ) ( ) Event of b₂ : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) SigmaField of b₁ : ( ( non empty ) ( non empty ) set ) ) ) ) : ( ( ) ( ext-real V14() real ) Element of REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) * (P : ( ( ) ( Relation-like b₂ : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) SigmaField of b₁ : ( ( non empty ) ( non empty ) set ) ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) -valued Function-like V30(b₂ : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) SigmaField of b₁ : ( ( non empty ) ( non empty ) set ) ) , REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) V35() V36() V37() V44() ) Probability of b₂ : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) SigmaField of b₁ : ( ( non empty ) ( non empty ) set ) ) ) . A2 : ( ( ) ( ) Event of b₂ : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) SigmaField of b₁ : ( ( non empty ) ( non empty ) set ) ) ) ) : ( ( ) ( ext-real V14() real ) Element of REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) ) : ( ( ) ( ext-real V14() real ) Element of REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) / (((((P : ( ( ) ( Relation-like b₂ : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) SigmaField of b₁ : ( ( non empty ) ( non empty ) set ) ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) -valued Function-like V30(b₂ : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) SigmaField of b₁ : ( ( non empty ) ( non empty ) set ) ) , REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) V35() V36() V37() V44() ) Probability of b₂ : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) SigmaField of b₁ : ( ( non empty ) ( non empty ) set ) ) ) .|. A1 : ( ( ) ( ) Event of b₂ : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) SigmaField of b₁ : ( ( non empty ) ( non empty ) set ) ) ) ) : ( ( ) ( Relation-like b₂ : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) SigmaField of b₁ : ( ( non empty ) ( non empty ) set ) ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) -valued Function-like V30(b₂ : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) SigmaField of b₁ : ( ( non empty ) ( non empty ) set ) ) , REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) V35() V36() V37() V44() ) Probability of b₂ : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) SigmaField of b₁ : ( ( non empty ) ( non empty ) set ) ) ) . B : ( ( ) ( ) Event of b₂ : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) SigmaField of b₁ : ( ( non empty ) ( non empty ) set ) ) ) ) : ( ( ) ( ext-real V14() real ) Element of REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) * (P : ( ( ) ( Relation-like b₂ : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) SigmaField of b₁ : ( ( non empty ) ( non empty ) set ) ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) -valued Function-like V30(b₂ : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) SigmaField of b₁ : ( ( non empty ) ( non empty ) set ) ) , REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) V35() V36() V37() V44() ) Probability of b₂ : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) SigmaField of b₁ : ( ( non empty ) ( non empty ) set ) ) ) . A1 : ( ( ) ( ) Event of b₂ : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) SigmaField of b₁ : ( ( non empty ) ( non empty ) set ) ) ) ) : ( ( ) ( ext-real V14() real ) Element of REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) ) : ( ( ) ( ext-real V14() real ) Element of REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) + (((P : ( ( ) ( Relation-like b₂ : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) SigmaField of b₁ : ( ( non empty ) ( non empty ) set ) ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) -valued Function-like V30(b₂ : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) SigmaField of b₁ : ( ( non empty ) ( non empty ) set ) ) , REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) V35() V36() V37() V44() ) Probability of b₂ : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) SigmaField of b₁ : ( ( non empty ) ( non empty ) set ) ) ) .|. A2 : ( ( ) ( ) Event of b₂ : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) SigmaField of b₁ : ( ( non empty ) ( non empty ) set ) ) ) ) : ( ( ) ( Relation-like b₂ : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) SigmaField of b₁ : ( ( non empty ) ( non empty ) set ) ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) -valued Function-like V30(b₂ : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) SigmaField of b₁ : ( ( non empty ) ( non empty ) set ) ) , REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) V35() V36() V37() V44() ) Probability of b₂ : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) SigmaField of b₁ : ( ( non empty ) ( non empty ) set ) ) ) . B : ( ( ) ( ) Event of b₂ : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) SigmaField of b₁ : ( ( non empty ) ( non empty ) set ) ) ) ) : ( ( ) ( ext-real V14() real ) Element of REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) * (P : ( ( ) ( Relation-like b₂ : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) SigmaField of b₁ : ( ( non empty ) ( non empty ) set ) ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) -valued Function-like V30(b₂ : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) SigmaField of b₁ : ( ( non empty ) ( non empty ) set ) ) , REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) V35() V36() V37() V44() ) Probability of b₂ : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) SigmaField of b₁ : ( ( non empty ) ( non empty ) set ) ) ) . A2 : ( ( ) ( ) Event of b₂ : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) SigmaField of b₁ : ( ( non empty ) ( non empty ) set ) ) ) ) : ( ( ) ( ext-real V14() real ) Element of REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) ) : ( ( ) ( ext-real V14() real ) Element of REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) ) : ( ( ) ( ext-real V14() real ) Element of REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) + (((P : ( ( ) ( Relation-like b₂ : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) SigmaField of b₁ : ( ( non empty ) ( non empty ) set ) ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) -valued Function-like V30(b₂ : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) SigmaField of b₁ : ( ( non empty ) ( non empty ) set ) ) , REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) V35() V36() V37() V44() ) Probability of b₂ : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) SigmaField of b₁ : ( ( non empty ) ( non empty ) set ) ) ) .|. A3 : ( ( ) ( ) Event of b₂ : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) SigmaField of b₁ : ( ( non empty ) ( non empty ) set ) ) ) ) : ( ( ) ( Relation-like b₂ : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) SigmaField of b₁ : ( ( non empty ) ( non empty ) set ) ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) -valued Function-like V30(b₂ : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) SigmaField of b₁ : ( ( non empty ) ( non empty ) set ) ) , REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) V35() V36() V37() V44() ) Probability of b₂ : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) SigmaField of b₁ : ( ( non empty ) ( non empty ) set ) ) ) . B : ( ( ) ( ) Event of b₂ : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) SigmaField of b₁ : ( ( non empty ) ( non empty ) set ) ) ) ) : ( ( ) ( ext-real V14() real ) Element of REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) * (P : ( ( ) ( Relation-like b₂ : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) SigmaField of b₁ : ( ( non empty ) ( non empty ) set ) ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) -valued Function-like V30(b₂ : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) SigmaField of b₁ : ( ( non empty ) ( non empty ) set ) ) , REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) V35() V36() V37() V44() ) Probability of b₂ : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) SigmaField of b₁ : ( ( non empty ) ( non empty ) set ) ) ) . A3 : ( ( ) ( ) Event of b₂ : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) SigmaField of b₁ : ( ( non empty ) ( non empty ) set ) ) ) ) : ( ( ) ( ext-real V14() real ) Element of REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) ) : ( ( ) ( ext-real V14() real ) Element of REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) ) : ( ( ) ( ext-real V14() real ) Element of REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ext-real V14() real ) Element of REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) & (P : ( ( ) ( Relation-like b₂ : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) SigmaField of b₁ : ( ( non empty ) ( non empty ) set ) ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) -valued Function-like V30(b₂ : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) SigmaField of b₁ : ( ( non empty ) ( non empty ) set ) ) , REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) V35() V36() V37() V44() ) Probability of b₂ : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) SigmaField of b₁ : ( ( non empty ) ( non empty ) set ) ) ) .|. B : ( ( ) ( ) Event of b₂ : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) SigmaField of b₁ : ( ( non empty ) ( non empty ) set ) ) ) ) : ( ( ) ( Relation-like b₂ : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) SigmaField of b₁ : ( ( non empty ) ( non empty ) set ) ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) -valued Function-like V30(b₂ : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) SigmaField of b₁ : ( ( non empty ) ( non empty ) set ) ) , REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) V35() V36() V37() V44() ) Probability of b₂ : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) SigmaField of b₁ : ( ( non empty ) ( non empty ) set ) ) ) . A3 : ( ( ) ( ) Event of b₂ : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) SigmaField of b₁ : ( ( non empty ) ( non empty ) set ) ) ) : ( ( ) ( ext-real V14() real ) Element of REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) = (((P : ( ( ) ( Relation-like b₂ : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) SigmaField of b₁ : ( ( non empty ) ( non empty ) set ) ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) -valued Function-like V30(b₂ : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) SigmaField of b₁ : ( ( non empty ) ( non empty ) set ) ) , REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) V35() V36() V37() V44() ) Probability of b₂ : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) SigmaField of b₁ : ( ( non empty ) ( non empty ) set ) ) ) .|. A3 : ( ( ) ( ) Event of b₂ : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) SigmaField of b₁ : ( ( non empty ) ( non empty ) set ) ) ) ) : ( ( ) ( Relation-like b₂ : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) SigmaField of b₁ : ( ( non empty ) ( non empty ) set ) ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) -valued Function-like V30(b₂ : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) SigmaField of b₁ : ( ( non empty ) ( non empty ) set ) ) , REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) V35() V36() V37() V44() ) Probability of b₂ : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) SigmaField of b₁ : ( ( non empty ) ( non empty ) set ) ) ) . B : ( ( ) ( ) Event of b₂ : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) SigmaField of b₁ : ( ( non empty ) ( non empty ) set ) ) ) ) : ( ( ) ( ext-real V14() real ) Element of REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) * (P : ( ( ) ( Relation-like b₂ : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) SigmaField of b₁ : ( ( non empty ) ( non empty ) set ) ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) -valued Function-like V30(b₂ : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) SigmaField of b₁ : ( ( non empty ) ( non empty ) set ) ) , REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) V35() V36() V37() V44() ) Probability of b₂ : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) SigmaField of b₁ : ( ( non empty ) ( non empty ) set ) ) ) . A3 : ( ( ) ( ) Event of b₂ : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) SigmaField of b₁ : ( ( non empty ) ( non empty ) set ) ) ) ) : ( ( ) ( ext-real V14() real ) Element of REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) ) : ( ( ) ( ext-real V14() real ) Element of REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) / (((((P : ( ( ) ( Relation-like b₂ : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) SigmaField of b₁ : ( ( non empty ) ( non empty ) set ) ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) -valued Function-like V30(b₂ : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) SigmaField of b₁ : ( ( non empty ) ( non empty ) set ) ) , REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) V35() V36() V37() V44() ) Probability of b₂ : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) SigmaField of b₁ : ( ( non empty ) ( non empty ) set ) ) ) .|. A1 : ( ( ) ( ) Event of b₂ : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) SigmaField of b₁ : ( ( non empty ) ( non empty ) set ) ) ) ) : ( ( ) ( Relation-like b₂ : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) SigmaField of b₁ : ( ( non empty ) ( non empty ) set ) ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) -valued Function-like V30(b₂ : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) SigmaField of b₁ : ( ( non empty ) ( non empty ) set ) ) , REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) V35() V36() V37() V44() ) Probability of b₂ : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) SigmaField of b₁ : ( ( non empty ) ( non empty ) set ) ) ) . B : ( ( ) ( ) Event of b₂ : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) SigmaField of b₁ : ( ( non empty ) ( non empty ) set ) ) ) ) : ( ( ) ( ext-real V14() real ) Element of REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) * (P : ( ( ) ( Relation-like b₂ : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) SigmaField of b₁ : ( ( non empty ) ( non empty ) set ) ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) -valued Function-like V30(b₂ : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) SigmaField of b₁ : ( ( non empty ) ( non empty ) set ) ) , REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) V35() V36() V37() V44() ) Probability of b₂ : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) SigmaField of b₁ : ( ( non empty ) ( non empty ) set ) ) ) . A1 : ( ( ) ( ) Event of b₂ : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) SigmaField of b₁ : ( ( non empty ) ( non empty ) set ) ) ) ) : ( ( ) ( ext-real V14() real ) Element of REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) ) : ( ( ) ( ext-real V14() real ) Element of REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) + (((P : ( ( ) ( Relation-like b₂ : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) SigmaField of b₁ : ( ( non empty ) ( non empty ) set ) ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) -valued Function-like V30(b₂ : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) SigmaField of b₁ : ( ( non empty ) ( non empty ) set ) ) , REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) V35() V36() V37() V44() ) Probability of b₂ : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) SigmaField of b₁ : ( ( non empty ) ( non empty ) set ) ) ) .|. A2 : ( ( ) ( ) Event of b₂ : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) SigmaField of b₁ : ( ( non empty ) ( non empty ) set ) ) ) ) : ( ( ) ( Relation-like b₂ : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) SigmaField of b₁ : ( ( non empty ) ( non empty ) set ) ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) -valued Function-like V30(b₂ : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) SigmaField of b₁ : ( ( non empty ) ( non empty ) set ) ) , REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) V35() V36() V37() V44() ) Probability of b₂ : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) SigmaField of b₁ : ( ( non empty ) ( non empty ) set ) ) ) . B : ( ( ) ( ) Event of b₂ : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) SigmaField of b₁ : ( ( non empty ) ( non empty ) set ) ) ) ) : ( ( ) ( ext-real V14() real ) Element of REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) * (P : ( ( ) ( Relation-like b₂ : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) SigmaField of b₁ : ( ( non empty ) ( non empty ) set ) ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) -valued Function-like V30(b₂ : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) SigmaField of b₁ : ( ( non empty ) ( non empty ) set ) ) , REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) V35() V36() V37() V44() ) Probability of b₂ : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) SigmaField of b₁ : ( ( non empty ) ( non empty ) set ) ) ) . A2 : ( ( ) ( ) Event of b₂ : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) SigmaField of b₁ : ( ( non empty ) ( non empty ) set ) ) ) ) : ( ( ) ( ext-real V14() real ) Element of REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) ) : ( ( ) ( ext-real V14() real ) Element of REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) ) : ( ( ) ( ext-real V14() real ) Element of REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) + (((P : ( ( ) ( Relation-like b₂ : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) SigmaField of b₁ : ( ( non empty ) ( non empty ) set ) ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) -valued Function-like V30(b₂ : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) SigmaField of b₁ : ( ( non empty ) ( non empty ) set ) ) , REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) V35() V36() V37() V44() ) Probability of b₂ : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) SigmaField of b₁ : ( ( non empty ) ( non empty ) set ) ) ) .|. A3 : ( ( ) ( ) Event of b₂ : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) SigmaField of b₁ : ( ( non empty ) ( non empty ) set ) ) ) ) : ( ( ) ( Relation-like b₂ : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) SigmaField of b₁ : ( ( non empty ) ( non empty ) set ) ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) -valued Function-like V30(b₂ : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) SigmaField of b₁ : ( ( non empty ) ( non empty ) set ) ) , REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) V35() V36() V37() V44() ) Probability of b₂ : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) SigmaField of b₁ : ( ( non empty ) ( non empty ) set ) ) ) . B : ( ( ) ( ) Event of b₂ : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) SigmaField of b₁ : ( ( non empty ) ( non empty ) set ) ) ) ) : ( ( ) ( ext-real V14() real ) Element of REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) * (P : ( ( ) ( Relation-like b₂ : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) SigmaField of b₁ : ( ( non empty ) ( non empty ) set ) ) -defined REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) -valued Function-like V30(b₂ : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) SigmaField of b₁ : ( ( non empty ) ( non empty ) set ) ) , REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) V35() V36() V37() V44() ) Probability of b₂ : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) SigmaField of b₁ : ( ( non empty ) ( non empty ) set ) ) ) . A3 : ( ( ) ( ) Event of b₂ : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative ) SigmaField of b₁ : ( ( non empty ) ( non empty ) set ) ) ) ) : ( ( ) ( ext-real V14() real ) Element of REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) ) : ( ( ) ( ext-real V14() real ) Element of REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) ) : ( ( ) ( ext-real V14() real ) Element of REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) : ( ( ) ( ext-real V14() real ) Element of REAL : ( ( ) ( non empty V45() V46() V47() V51() V52() ) set ) ) ) ;

theorem :: PROB_2:39