K92() is V23() V29() cardinal limit_cardinal Element of K19(K88())
K88() is set
K19(K88()) is set
K87() is V23() V29() cardinal limit_cardinal set
K19(K87()) is V29() set
K19(K92()) is V29() set
2 is non empty set
[#] (2,2) is Relation-like set
[#] (([#] (2,2)),2) is Relation-like set
K19(([#] (([#] (2,2)),2))) is set
[#] (K92(),K88()) is Relation-like set
K19(([#] (K92(),K88()))) is set
K19(K19(K88())) is set
K335() is non empty V225(K88()) V228(K88()) Element of K19(K19(K88()))
1 is non empty set
[#] (1,1) is Relation-like set
K19(([#] (1,1))) is set
[#] (([#] (1,1)),1) is Relation-like set
K19(([#] (([#] (1,1)),1))) is set
K419() is set
Probabilities K335() is set
{} is Relation-like non-empty empty-yielding Function-like one-to-one constant functional empty V23() cardinal {} -element reflexive irreflexive symmetric antisymmetric asymmetric connected strongly_connected transitive set
op1 is Relation-like Function-like non empty V14(1) V18(1,1) involutive Element of K19(([#] (1,1)))
[{},{}] is set
{[{},{}]} is Relation-like Function-like constant non empty V12() 1 -element set
{{}} is functional non empty V12() 1 -element set
c1 is non empty reflexive antisymmetric RelStr
the carrier of c1 is non empty set
C is Element of the carrier of c1
S is Element of the carrier of c1
{C,S} is non empty Element of K19( the carrier of c1)
K19( the carrier of c1) is set
"\/" ({C,S},c1) is Element of the carrier of c1
"/\" ({C,S},c1) is Element of the carrier of c1
f is Element of the carrier of c1
f is Element of the carrier of c1
f is Element of {C,S}
f is Element of the carrier of c1
f is Element of the carrier of c1
c1 is set
[#] (c1,c1) is Relation-like set
K19(([#] (c1,c1))) is set
{} (c1,c1) is Relation-like non-empty empty-yielding Function-like one-to-one constant functional empty V23() cardinal {} -element reflexive irreflexive symmetric antisymmetric asymmetric connected strongly_connected transitive Element of K19(([#] (c1,c1)))
c1 is non empty set
[#] (c1,c1) is Relation-like set
K19(([#] (c1,c1))) is set
C is Relation-like Element of K19(([#] (c1,c1)))
S is Relation-like Function-like non empty V14(c1) V18(c1,c1) Element of K19(([#] (c1,c1)))
OrthoRelStr(# c1,C,S #) is strict OrthoRelStr
the non empty set is non empty set
[#] ( the non empty set , the non empty set ) is Relation-like set
K19(([#] ( the non empty set , the non empty set ))) is set
the Relation-like Element of K19(([#] ( the non empty set , the non empty set ))) is Relation-like Element of K19(([#] ( the non empty set , the non empty set )))
the Relation-like Function-like non empty V14( the non empty set ) V18( the non empty set , the non empty set ) Element of K19(([#] ( the non empty set , the non empty set ))) is Relation-like Function-like non empty V14( the non empty set ) V18( the non empty set , the non empty set ) Element of K19(([#] ( the non empty set , the non empty set )))
OrthoRelStr(# the non empty set , the Relation-like Element of K19(([#] ( the non empty set , the non empty set ))), the Relation-like Function-like non empty V14( the non empty set ) V18( the non empty set , the non empty set ) Element of K19(([#] ( the non empty set , the non empty set ))) #) is non empty strict OrthoRelStr
c1 is set
[#] (c1,c1) is Relation-like set
K19(([#] (c1,c1))) is set
id c1 is Relation-like c1 -defined c1 -valued Function-like one-to-one V14(c1) V18(c1,c1) V19(c1) V20(c1,c1) reflexive symmetric antisymmetric transitive involutive Element of K19(([#] (c1,c1)))
id 1 is Relation-like 1 -defined 1 -valued Function-like one-to-one non empty V14(1) V18(1,1) V19(1) V20(1,1) reflexive symmetric antisymmetric transitive involutive Element of K19(([#] (1,1)))
OrthoRelStr(# 1,(id 1),op1 #) is non empty strict OrthoRelStr
() is strict OrthoRelStr
the carrier of () is set
{} (1,1) is Relation-like non-empty empty-yielding Function-like one-to-one constant functional empty V23() cardinal {} -element reflexive irreflexive symmetric antisymmetric asymmetric connected strongly_connected transitive Element of K19(([#] (1,1)))
OrthoRelStr(# 1,({} (1,1)),op1 #) is non empty strict OrthoRelStr
() is strict OrthoRelStr
c1 is non empty RelStr
the InternalRel of c1 is Relation-like Element of K19(([#] ( the carrier of c1, the carrier of c1)))
the carrier of c1 is non empty set
[#] ( the carrier of c1, the carrier of c1) is Relation-like set
K19(([#] ( the carrier of c1, the carrier of c1))) is set
id {{}} is Relation-like {{}} -defined {{}} -valued Function-like one-to-one non empty V14({{}}) V18({{}},{{}}) V19({{}}) V20({{}},{{}}) reflexive symmetric antisymmetric transitive involutive Element of K19(([#] ({{}},{{}})))
[#] ({{}},{{}}) is Relation-like set
K19(([#] ({{}},{{}}))) is set
rng (id {{}}) is non empty set
field (id {{}}) is set
dom (id {{}}) is non empty set
(dom (id {{}})) \/ (rng (id {{}})) is non empty set
c1 is non empty RelStr
the InternalRel of c1 is Relation-like Element of K19(([#] ( the carrier of c1, the carrier of c1)))
the carrier of c1 is non empty set
[#] ( the carrier of c1, the carrier of c1) is Relation-like set
K19(([#] ( the carrier of c1, the carrier of c1))) is set
field the InternalRel of c1 is set
dom the InternalRel of c1 is set
rng the InternalRel of c1 is set
(dom the InternalRel of c1) \/ (rng the InternalRel of c1) is set
the carrier of c1 \/ the carrier of c1 is non empty set
S is set
[S,S] is set
S is set
[S,S] is set
C is set
[C,C] is set
C is set
[C,C] is set
{} ({{}},{{}}) is Relation-like non-empty empty-yielding Function-like one-to-one constant functional empty V23() cardinal {} -element reflexive irreflexive symmetric antisymmetric asymmetric connected strongly_connected transitive Element of K19(([#] ({{}},{{}})))
[#] ({{}},{{}}) is Relation-like set
K19(([#] ({{}},{{}}))) is set
c1 is set
[c1,c1] is set
c1 is non empty RelStr
the InternalRel of c1 is Relation-like Element of K19(([#] ( the carrier of c1, the carrier of c1)))
the carrier of c1 is non empty set
[#] ( the carrier of c1, the carrier of c1) is Relation-like set
K19(([#] ( the carrier of c1, the carrier of c1))) is set
c1 is non empty RelStr
the InternalRel of c1 is Relation-like Element of K19(([#] ( the carrier of c1, the carrier of c1)))
the carrier of c1 is non empty set
[#] ( the carrier of c1, the carrier of c1) is Relation-like set
K19(([#] ( the carrier of c1, the carrier of c1))) is set
c1 is non empty RelStr
the InternalRel of c1 is Relation-like Element of K19(([#] ( the carrier of c1, the carrier of c1)))
the carrier of c1 is non empty set
[#] ( the carrier of c1, the carrier of c1) is Relation-like set
K19(([#] ( the carrier of c1, the carrier of c1))) is set
c1 is non empty RelStr
the InternalRel of c1 is Relation-like Element of K19(([#] ( the carrier of c1, the carrier of c1)))
the carrier of c1 is non empty set
[#] ( the carrier of c1, the carrier of c1) is Relation-like set
K19(([#] ( the carrier of c1, the carrier of c1))) is set
c1 is non empty RelStr
the InternalRel of c1 is Relation-like Element of K19(([#] ( the carrier of c1, the carrier of c1)))
the carrier of c1 is non empty set
[#] ( the carrier of c1, the carrier of c1) is Relation-like set
K19(([#] ( the carrier of c1, the carrier of c1))) is set
c1 is non empty RelStr
the InternalRel of c1 is Relation-like Element of K19(([#] ( the carrier of c1, the carrier of c1)))
the carrier of c1 is non empty set
[#] ( the carrier of c1, the carrier of c1) is Relation-like set
K19(([#] ( the carrier of c1, the carrier of c1))) is set
c1 is non empty RelStr
the InternalRel of c1 is Relation-like Element of K19(([#] ( the carrier of c1, the carrier of c1)))
the carrier of c1 is non empty set
[#] ( the carrier of c1, the carrier of c1) is Relation-like set
K19(([#] ( the carrier of c1, the carrier of c1))) is set
c1 is non empty RelStr
the InternalRel of c1 is Relation-like Element of K19(([#] ( the carrier of c1, the carrier of c1)))
the carrier of c1 is non empty set
[#] ( the carrier of c1, the carrier of c1) is Relation-like set
K19(([#] ( the carrier of c1, the carrier of c1))) is set
c1 is non empty OrthoRelStr
c1 is non empty OrthoRelStr
c1 is non empty OrthoRelStr
c1 is non empty OrthoRelStr
c1 is non empty OrthoRelStr
c1 is non empty OrthoRelStr
c1 is non empty () () OrthoRelStr
c1 is non empty OrthoRelStr
c1 is non empty RelStr
the carrier of c1 is non empty set
[#] ( the carrier of c1, the carrier of c1) is Relation-like set
K19(([#] ( the carrier of c1, the carrier of c1))) is set
the Compl of () is Relation-like Function-like non empty V14( the carrier of ()) V18( the carrier of (), the carrier of ()) Element of K19(([#] ( the carrier of (), the carrier of ())))
the carrier of () is non empty V12() V29() 1 -element set
[#] ( the carrier of (), the carrier of ()) is Relation-like set
K19(([#] ( the carrier of (), the carrier of ()))) is set
f is Relation-like Function-like non empty V14( the carrier of ()) V18( the carrier of (), the carrier of ()) Element of K19(([#] ( the carrier of (), the carrier of ())))
f is Element of the carrier of ()
a is Element of the carrier of ()
f . f is Element of the carrier of ()
f . a is Element of the carrier of ()
S is Element of the carrier of ()
c8 is Element of the carrier of ()
c9 is Element of the carrier of ()
c1 is non empty RelStr
the carrier of c1 is non empty set
[#] ( the carrier of c1, the carrier of c1) is Relation-like set
K19(([#] ( the carrier of c1, the carrier of c1))) is set
id {{}} is Relation-like {{}} -defined {{}} -valued Function-like one-to-one non empty V14({{}}) V18({{}},{{}}) V19({{}}) V20({{}},{{}}) reflexive symmetric antisymmetric transitive involutive Element of K19(([#] ({{}},{{}})))
[#] ({{}},{{}}) is Relation-like set
K19(([#] ({{}},{{}}))) is set
f is Element of the carrier of ()
op1 . f is set
{f,(op1 . f)} is non empty set
{f} is non empty V12() 1 -element Element of K19( the carrier of ())
K19( the carrier of ()) is set
f is Relation-like Function-like non empty V14( the carrier of ()) V18( the carrier of (), the carrier of ()) Element of K19(([#] ( the carrier of (), the carrier of ())))
f is Element of the carrier of ()
f . f is Element of the carrier of ()
{f,(f . f)} is non empty Element of K19( the carrier of ())
K19( the carrier of ()) is set
"\/" ({f,(f . f)},()) is Element of the carrier of ()
"/\" ({f,(f . f)},()) is Element of the carrier of ()
{f} is non empty V12() 1 -element Element of K19( the carrier of ())
c1 is non empty RelStr
the carrier of c1 is non empty set
[#] ( the carrier of c1, the carrier of c1) is Relation-like set
K19(([#] ( the carrier of c1, the carrier of c1))) is set
c1 is non empty OrthoRelStr
the carrier of c1 is non empty set
[#] ( the carrier of c1, the carrier of c1) is Relation-like set
K19(([#] ( the carrier of c1, the carrier of c1))) is set
C is Relation-like Function-like non empty V14( the carrier of c1) V18( the carrier of c1, the carrier of c1) Element of K19(([#] ( the carrier of c1, the carrier of c1)))
S is Element of the carrier of c1
C . S is Element of the carrier of c1
{S,(C . S)} is non empty Element of K19( the carrier of c1)
K19( the carrier of c1) is set
f is Element of the carrier of c1
C . f is Element of the carrier of c1
{f,(C . f)} is non empty Element of K19( the carrier of c1)
f is Relation-like Function-like non empty V14( the carrier of ()) V18( the carrier of (), the carrier of ()) Element of K19(([#] ( the carrier of (), the carrier of ())))
a is Element of the carrier of ()
op1 . a is set
{a,(op1 . a)} is non empty set
{a} is non empty V12() 1 -element Element of K19( the carrier of ())
K19( the carrier of ()) is set
f is Relation-like Function-like non empty V14( the carrier of ()) V18( the carrier of (), the carrier of ()) Element of K19(([#] ( the carrier of (), the carrier of ())))
a is Element of the carrier of ()
f . a is Element of the carrier of ()
{a,(f . a)} is non empty Element of K19( the carrier of ())
K19( the carrier of ()) is set
"\/" ({a,(f . a)},()) is Element of the carrier of ()
"/\" ({a,(f . a)},()) is Element of the carrier of ()
{a} is non empty V12() 1 -element Element of K19( the carrier of ())
a is Element of the carrier of ()
f . a is Element of the carrier of ()
{a,(f . a)} is non empty Element of K19( the carrier of ())
K19( the carrier of ()) is set
"\/" ({a,(f . a)},()) is Element of the carrier of ()
"/\" ({a,(f . a)},()) is Element of the carrier of ()
a is Element of the carrier of ()
f . a is Element of the carrier of ()
{a,(f . a)} is non empty Element of K19( the carrier of ())
K19( the carrier of ()) is set
"\/" ({a,(f . a)},()) is Element of the carrier of ()
"/\" ({a,(f . a)},()) is Element of the carrier of ()
a is Element of the carrier of ()
f . a is Element of the carrier of ()
{a,(f . a)} is non empty Element of K19( the carrier of ())
K19( the carrier of ()) is set
"\/" ({a,(f . a)},()) is Element of the carrier of ()
"/\" ({a,(f . a)},()) is Element of the carrier of ()
a0 is Element of the carrier of ()
f . a0 is Element of the carrier of ()
{a0,(f . a0)} is non empty Element of K19( the carrier of ())
{a0} is non empty V12() 1 -element Element of K19( the carrier of ())