:: OPOSET_1 semantic presentation

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

c

the carrier of c

C is Element of the carrier of c

S is Element of the carrier of c

{C,S} is non empty Element of K19( the carrier of c

K19( the carrier of c

"\/" ({C,S},c

"/\" ({C,S},c

f is Element of the carrier of c

f is Element of the carrier of c

f is Element of {C,S}

f is Element of the carrier of c

f is Element of the carrier of c

c

[#] (c

K19(([#] (c

{} (c

c

[#] (c

K19(([#] (c

C is Relation-like Element of K19(([#] (c

S is Relation-like Function-like non empty V14(c

OrthoRelStr(# c

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

c

[#] (c

K19(([#] (c

id c

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

c

the InternalRel of c

the carrier of c

[#] ( the carrier of c

K19(([#] ( the carrier of c

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

c

the InternalRel of c

the carrier of c

[#] ( the carrier of c

K19(([#] ( the carrier of c

field the InternalRel of c

dom the InternalRel of c

rng the InternalRel of c

(dom the InternalRel of c

the carrier of c

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

c

[c

c

the InternalRel of c

the carrier of c

[#] ( the carrier of c

K19(([#] ( the carrier of c

c

the InternalRel of c

the carrier of c

[#] ( the carrier of c

K19(([#] ( the carrier of c

c

the InternalRel of c

the carrier of c

[#] ( the carrier of c

K19(([#] ( the carrier of c

c

the InternalRel of c

the carrier of c

[#] ( the carrier of c

K19(([#] ( the carrier of c

c

the InternalRel of c

the carrier of c

[#] ( the carrier of c

K19(([#] ( the carrier of c

c

the InternalRel of c

the carrier of c

[#] ( the carrier of c

K19(([#] ( the carrier of c

c

the InternalRel of c

the carrier of c

[#] ( the carrier of c

K19(([#] ( the carrier of c

c

the InternalRel of c

the carrier of c

[#] ( the carrier of c

K19(([#] ( the carrier of c

c

c

c

c

c

c

c

c

c

the carrier of c

[#] ( the carrier of c

K19(([#] ( the carrier of c

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 ()

c

c

c

the carrier of c

[#] ( the carrier of c

K19(([#] ( the carrier of c

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 ())

c

the carrier of c

[#] ( the carrier of c

K19(([#] ( the carrier of c

c

the carrier of c

[#] ( the carrier of c

K19(([#] ( the carrier of c

C is Relation-like Function-like non empty V14( the carrier of c

S is Element of the carrier of c

C . S is Element of the carrier of c

{S,(C . S)} is non empty Element of K19( the carrier of c

K19( the carrier of c

f is Element of the carrier of c

C . f is Element of the carrier of c

{f,(C . f)} is non empty Element of K19( the carrier of c

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 ())