:: LATSUM_1 semantic presentation

K88() is set
K19(K88()) is set
{} is empty set
1 is non empty set
R is set
X is set
F is set
X \/ F is set
S is set
X \ F is Element of K19(X)
K19(X) is set
(X \ F) \/ F is set
R is RelStr
the carrier of R is set
S is RelStr
the carrier of S is set
the carrier of R \/ the carrier of S is set
the InternalRel of R is V1() V4( the carrier of R) V5( the carrier of R) Element of K19(K20( the carrier of R, the carrier of R))
K20( the carrier of R, the carrier of R) is set
K19(K20( the carrier of R, the carrier of R)) is set
the InternalRel of S is V1() V4( the carrier of S) V5( the carrier of S) Element of K19(K20( the carrier of S, the carrier of S))
K20( the carrier of S, the carrier of S) is set
K19(K20( the carrier of S, the carrier of S)) is set
the InternalRel of R \/ the InternalRel of S is set
the InternalRel of R * the InternalRel of S is V1() V4( the carrier of R) V5( the carrier of S) Element of K19(K20( the carrier of R, the carrier of S))
K20( the carrier of R, the carrier of S) is set
K19(K20( the carrier of R, the carrier of S)) is set
( the InternalRel of R \/ the InternalRel of S) \/ ( the InternalRel of R * the InternalRel of S) is set
K20(( the carrier of R \/ the carrier of S),( the carrier of R \/ the carrier of S)) is set
K19(K20(( the carrier of R \/ the carrier of S),( the carrier of R \/ the carrier of S))) is set
x is V1() V4( the carrier of R \/ the carrier of S) V5( the carrier of R \/ the carrier of S) Element of K19(K20(( the carrier of R \/ the carrier of S),( the carrier of R \/ the carrier of S)))
y is V1() V4( the carrier of R \/ the carrier of S) V5( the carrier of R \/ the carrier of S) Element of K19(K20(( the carrier of R \/ the carrier of S),( the carrier of R \/ the carrier of S)))
x \/ y is V1() V4( the carrier of R \/ the carrier of S) V5( the carrier of R \/ the carrier of S) Element of K19(K20(( the carrier of R \/ the carrier of S),( the carrier of R \/ the carrier of S)))
F is V1() V4( the carrier of R \/ the carrier of S) V5( the carrier of R \/ the carrier of S) Element of K19(K20(( the carrier of R \/ the carrier of S),( the carrier of R \/ the carrier of S)))
(x \/ y) \/ F is V1() V4( the carrier of R \/ the carrier of S) V5( the carrier of R \/ the carrier of S) Element of K19(K20(( the carrier of R \/ the carrier of S),( the carrier of R \/ the carrier of S)))
a is V1() V4( the carrier of R \/ the carrier of S) V5( the carrier of R \/ the carrier of S) Element of K19(K20(( the carrier of R \/ the carrier of S),( the carrier of R \/ the carrier of S)))
RelStr(# ( the carrier of R \/ the carrier of S),a #) is strict RelStr
the carrier of RelStr(# ( the carrier of R \/ the carrier of S),a #) is set
the InternalRel of RelStr(# ( the carrier of R \/ the carrier of S),a #) is V1() V4( the carrier of RelStr(# ( the carrier of R \/ the carrier of S),a #)) V5( the carrier of RelStr(# ( the carrier of R \/ the carrier of S),a #)) Element of K19(K20( the carrier of RelStr(# ( the carrier of R \/ the carrier of S),a #), the carrier of RelStr(# ( the carrier of R \/ the carrier of S),a #)))
K20( the carrier of RelStr(# ( the carrier of R \/ the carrier of S),a #), the carrier of RelStr(# ( the carrier of R \/ the carrier of S),a #)) is set
K19(K20( the carrier of RelStr(# ( the carrier of R \/ the carrier of S),a #), the carrier of RelStr(# ( the carrier of R \/ the carrier of S),a #))) is set
X is strict RelStr
the carrier of X is set
the InternalRel of X is V1() V4( the carrier of X) V5( the carrier of X) Element of K19(K20( the carrier of X, the carrier of X))
K20( the carrier of X, the carrier of X) is set
K19(K20( the carrier of X, the carrier of X)) is set
F is strict RelStr
the carrier of F is set
the InternalRel of F is V1() V4( the carrier of F) V5( the carrier of F) Element of K19(K20( the carrier of F, the carrier of F))
K20( the carrier of F, the carrier of F) is set
K19(K20( the carrier of F, the carrier of F)) is set
R is RelStr
S is non empty RelStr
(R,S) is strict RelStr
the carrier of R is set
the carrier of S is non empty set
the carrier of R \/ the carrier of S is non empty set
R is non empty RelStr
S is RelStr
(R,S) is strict RelStr
the carrier of R is non empty set
the carrier of S is set
the carrier of R \/ the carrier of S is non empty set
R is RelStr
the carrier of R is set
the InternalRel of R is V1() V4( the carrier of R) V5( the carrier of R) Element of K19(K20( the carrier of R, the carrier of R))
K20( the carrier of R, the carrier of R) is set
K19(K20( the carrier of R, the carrier of R)) is set
S is RelStr
(R,S) is strict RelStr
the InternalRel of (R,S) is V1() V4( the carrier of (R,S)) V5( the carrier of (R,S)) Element of K19(K20( the carrier of (R,S), the carrier of (R,S)))
the carrier of (R,S) is set
K20( the carrier of (R,S), the carrier of (R,S)) is set
K19(K20( the carrier of (R,S), the carrier of (R,S))) is set
the carrier of S is set
the InternalRel of S is V1() V4( the carrier of S) V5( the carrier of S) Element of K19(K20( the carrier of S, the carrier of S))
K20( the carrier of S, the carrier of S) is set
K19(K20( the carrier of S, the carrier of S)) is set
the InternalRel of R \/ the InternalRel of S is set
the InternalRel of R * the InternalRel of S is V1() V4( the carrier of R) V5( the carrier of S) Element of K19(K20( the carrier of R, the carrier of S))
K20( the carrier of R, the carrier of S) is set
K19(K20( the carrier of R, the carrier of S)) is set
( the InternalRel of R \/ the InternalRel of S) \/ ( the InternalRel of R * the InternalRel of S) is set
R is RelStr
S is RelStr
(R,S) is strict RelStr
the InternalRel of R is V1() V4( the carrier of R) V5( the carrier of R) Element of K19(K20( the carrier of R, the carrier of R))
the carrier of R is set
K20( the carrier of R, the carrier of R) is set
K19(K20( the carrier of R, the carrier of R)) is set
the InternalRel of S is V1() V4( the carrier of S) V5( the carrier of S) Element of K19(K20( the carrier of S, the carrier of S))
the carrier of S is set
K20( the carrier of S, the carrier of S) is set
K19(K20( the carrier of S, the carrier of S)) is set
the InternalRel of (R,S) is V1() V4( the carrier of (R,S)) V5( the carrier of (R,S)) Element of K19(K20( the carrier of (R,S), the carrier of (R,S)))
the carrier of (R,S) is set
K20( the carrier of (R,S), the carrier of (R,S)) is set
K19(K20( the carrier of (R,S), the carrier of (R,S))) is set
X is set
[X,X] is set
the carrier of R \/ the carrier of S is set
R is RelStr
S is RelStr
(R,S) is strict RelStr
the InternalRel of (R,S) is V1() V4( the carrier of (R,S)) V5( the carrier of (R,S)) Element of K19(K20( the carrier of (R,S), the carrier of (R,S)))
the carrier of (R,S) is set
K20( the carrier of (R,S), the carrier of (R,S)) is set
K19(K20( the carrier of (R,S), the carrier of (R,S))) is set
the carrier of R is set
the InternalRel of R is V1() V4( the carrier of R) V5( the carrier of R) Element of K19(K20( the carrier of R, the carrier of R))
K20( the carrier of R, the carrier of R) is set
K19(K20( the carrier of R, the carrier of R)) is set
X is set
F is set
[X,F] is set
the InternalRel of S is V1() V4( the carrier of S) V5( the carrier of S) Element of K19(K20( the carrier of S, the carrier of S))
the carrier of S is set
K20( the carrier of S, the carrier of S) is set
K19(K20( the carrier of S, the carrier of S)) is set
the InternalRel of R \/ the InternalRel of S is set
the InternalRel of R * the InternalRel of S is V1() V4( the carrier of R) V5( the carrier of S) Element of K19(K20( the carrier of R, the carrier of S))
K20( the carrier of R, the carrier of S) is set
K19(K20( the carrier of R, the carrier of S)) is set
( the InternalRel of R \/ the InternalRel of S) \/ ( the InternalRel of R * the InternalRel of S) is set
the carrier of R /\ the carrier of S is set
the carrier of R /\ the carrier of S is set
x is set
[X,x] is set
[x,F] is set
R is RelStr
S is RelStr
(R,S) is strict RelStr
the InternalRel of (R,S) is V1() V4( the carrier of (R,S)) V5( the carrier of (R,S)) Element of K19(K20( the carrier of (R,S), the carrier of (R,S)))
the carrier of (R,S) is set
K20( the carrier of (R,S), the carrier of (R,S)) is set
K19(K20( the carrier of (R,S), the carrier of (R,S))) is set
the carrier of S is set
the InternalRel of S is V1() V4( the carrier of S) V5( the carrier of S) Element of K19(K20( the carrier of S, the carrier of S))
K20( the carrier of S, the carrier of S) is set
K19(K20( the carrier of S, the carrier of S)) is set
X is set
F is set
[X,F] is set
the InternalRel of R is V1() V4( the carrier of R) V5( the carrier of R) Element of K19(K20( the carrier of R, the carrier of R))
the carrier of R is set
K20( the carrier of R, the carrier of R) is set
K19(K20( the carrier of R, the carrier of R)) is set
the InternalRel of R \/ the InternalRel of S is set
the InternalRel of R * the InternalRel of S is V1() V4( the carrier of R) V5( the carrier of S) Element of K19(K20( the carrier of R, the carrier of S))
K20( the carrier of R, the carrier of S) is set
K19(K20( the carrier of R, the carrier of S)) is set
( the InternalRel of R \/ the InternalRel of S) \/ ( the InternalRel of R * the InternalRel of S) is set
the carrier of R /\ the carrier of S is set
the carrier of R /\ the carrier of S is set
x is set
[X,x] is set
[x,F] is set
R is RelStr
the InternalRel of R is V1() V4( the carrier of R) V5( the carrier of R) Element of K19(K20( the carrier of R, the carrier of R))
the carrier of R is set
K20( the carrier of R, the carrier of R) is set
K19(K20( the carrier of R, the carrier of R)) is set
S is RelStr
(R,S) is strict RelStr
the InternalRel of (R,S) is V1() V4( the carrier of (R,S)) V5( the carrier of (R,S)) Element of K19(K20( the carrier of (R,S), the carrier of (R,S)))
the carrier of (R,S) is set
K20( the carrier of (R,S), the carrier of (R,S)) is set
K19(K20( the carrier of (R,S), the carrier of (R,S))) is set
the InternalRel of S is V1() V4( the carrier of S) V5( the carrier of S) Element of K19(K20( the carrier of S, the carrier of S))
the carrier of S is set
K20( the carrier of S, the carrier of S) is set
K19(K20( the carrier of S, the carrier of S)) is set
X is set
F is set
[X,F] is set
the InternalRel of R \/ the InternalRel of S is set
the InternalRel of R * the InternalRel of S is V1() V4( the carrier of R) V5( the carrier of S) Element of K19(K20( the carrier of R, the carrier of S))
K20( the carrier of R, the carrier of S) is set
K19(K20( the carrier of R, the carrier of S)) is set
( the InternalRel of R \/ the InternalRel of S) \/ ( the InternalRel of R * the InternalRel of S) is set
the InternalRel of R \/ the InternalRel of S is set
the InternalRel of R * the InternalRel of S is V1() V4( the carrier of R) V5( the carrier of S) Element of K19(K20( the carrier of R, the carrier of S))
K20( the carrier of R, the carrier of S) is set
K19(K20( the carrier of R, the carrier of S)) is set
( the InternalRel of R \/ the InternalRel of S) \/ ( the InternalRel of R * the InternalRel of S) is set
R is non empty RelStr
S is non empty RelStr
(R,S) is non empty strict RelStr
the carrier of (R,S) is non empty set
the carrier of R is non empty set
the carrier of S is non empty set
the carrier of S \ the carrier of R is Element of K19( the carrier of S)
K19( the carrier of S) is set
X is Element of the carrier of (R,S)
the carrier of S \/ the carrier of R is non empty set
the carrier of R \/ ( the carrier of S \ the carrier of R) is non empty set
R is non empty RelStr
the carrier of R is non empty set
S is non empty RelStr
(R,S) is non empty strict RelStr
the carrier of (R,S) is non empty set
X is Element of the carrier of R
F is Element of the carrier of R
x is Element of the carrier of (R,S)
y is Element of the carrier of (R,S)
[X,F] is set
the InternalRel of R is V1() V4( the carrier of R) V5( the carrier of R) Element of K19(K20( the carrier of R, the carrier of R))
K20( the carrier of R, the carrier of R) is set
K19(K20( the carrier of R, the carrier of R)) is set
[x,y] is set
the InternalRel of (R,S) is V1() V4( the carrier of (R,S)) V5( the carrier of (R,S)) Element of K19(K20( the carrier of (R,S), the carrier of (R,S)))
K20( the carrier of (R,S), the carrier of (R,S)) is set
K19(K20( the carrier of (R,S), the carrier of (R,S))) is set
R is non empty RelStr
S is non empty RelStr
(R,S) is non empty strict RelStr
the carrier of (R,S) is non empty set
the carrier of S is non empty set
X is Element of the carrier of (R,S)
F is Element of the carrier of (R,S)
x is Element of the carrier of S
y is Element of the carrier of S
[X,F] is set
the InternalRel of (R,S) is V1() V4( the carrier of (R,S)) V5( the carrier of (R,S)) Element of K19(K20( the carrier of (R,S), the carrier of (R,S)))
K20( the carrier of (R,S), the carrier of (R,S)) is set
K19(K20( the carrier of (R,S), the carrier of (R,S))) is set
[x,y] is set
the InternalRel of S is V1() V4( the carrier of S) V5( the carrier of S) Element of K19(K20( the carrier of S, the carrier of S))
K20( the carrier of S, the carrier of S) is set
K19(K20( the carrier of S, the carrier of S)) is set
R is non empty reflexive transitive antisymmetric with_suprema RelStr
the carrier of R is non empty set
S is non empty reflexive transitive antisymmetric with_suprema RelStr
(R,S) is non empty strict RelStr
the carrier of (R,S) is non empty set
X is set
the carrier of S is non empty set
the carrier of R \/ the carrier of S is non empty set
S is non empty reflexive transitive antisymmetric with_suprema RelStr
the carrier of S is non empty set
R is non empty reflexive transitive antisymmetric with_suprema RelStr
(R,S) is non empty strict RelStr
the carrier of (R,S) is non empty set
X is set
the carrier of R is non empty set
the carrier of R \/ the carrier of S is non empty set
R is non empty RelStr
the carrier of R is non empty set
S is non empty RelStr
the carrier of S is non empty set
the carrier of R /\ the carrier of S is set
X is set
R is non empty RelStr
the carrier of R is non empty set
S is non empty RelStr
the carrier of S is non empty set
the carrier of R /\ the carrier of S is set
X is set
R is non empty reflexive transitive antisymmetric with_suprema RelStr
S is non empty reflexive transitive antisymmetric with_suprema RelStr
(R,S) is non empty strict RelStr
the carrier of (R,S) is non empty set
the carrier of R is non empty set
the carrier of S is non empty set
the carrier of R /\ the carrier of S is set
X is Element of the carrier of (R,S)
F is Element of the carrier of (R,S)
[X,F] is set
the InternalRel of R is V1() V4( the carrier of R) V5( the carrier of R) Element of K19(K20( the carrier of R, the carrier of R))
K20( the carrier of R, the carrier of R) is set
K19(K20( the carrier of R, the carrier of R)) is set
x is Element of the carrier of (R,S)
the InternalRel of (R,S) is V1() V4( the carrier of (R,S)) V5( the carrier of (R,S)) Element of K19(K20( the carrier of (R,S), the carrier of (R,S)))
K20( the carrier of (R,S), the carrier of (R,S)) is set
K19(K20( the carrier of (R,S), the carrier of (R,S))) is set
x is Element of the carrier of (R,S)
[X,F] is set
the InternalRel of S is V1() V4( the carrier of S) V5( the carrier of S) Element of K19(K20( the carrier of S, the carrier of S))
K20( the carrier of S, the carrier of S) is set
K19(K20( the carrier of S, the carrier of S)) is set
x is Element of the carrier of (R,S)
the InternalRel of (R,S) is V1() V4( the carrier of (R,S)) V5( the carrier of (R,S)) Element of K19(K20( the carrier of (R,S), the carrier of (R,S)))
K20( the carrier of (R,S), the carrier of (R,S)) is set
K19(K20( the carrier of (R,S), the carrier of (R,S))) is set
x is Element of the carrier of (R,S)
[X,F] is set
the InternalRel of R is V1() V4( the carrier of R) V5( the carrier of R) Element of K19(K20( the carrier of R, the carrier of R))
K20( the carrier of R, the carrier of R) is set
K19(K20( the carrier of R, the carrier of R)) is set
the InternalRel of S is V1() V4( the carrier of S) V5( the carrier of S) Element of K19(K20( the carrier of S, the carrier of S))
K20( the carrier of S, the carrier of S) is set
K19(K20( the carrier of S, the carrier of S)) is set
the InternalRel of (R,S) is V1() V4( the carrier of (R,S)) V5( the carrier of (R,S)) Element of K19(K20( the carrier of (R,S), the carrier of (R,S)))
K20( the carrier of (R,S), the carrier of (R,S)) is set
K19(K20( the carrier of (R,S), the carrier of (R,S))) is set
the InternalRel of R \/ the InternalRel of S is set
the InternalRel of R * the InternalRel of S is V1() V4( the carrier of R) V5( the carrier of S) Element of K19(K20( the carrier of R, the carrier of S))
K20( the carrier of R, the carrier of S) is set
K19(K20( the carrier of R, the carrier of S)) is set
( the InternalRel of R \/ the InternalRel of S) \/ ( the InternalRel of R * the InternalRel of S) is set
x is set
[X,x] is set
[x,F] is set
the carrier of R \/ the carrier of S is non empty set
y is Element of the carrier of (R,S)
z is Element of the carrier of (R,S)
[X,z] is set
[z,F] is set
x is Element of the carrier of (R,S)
z is Element of the carrier of S
y is Element of the carrier of S
[x,F] is set
a is Element of the carrier of R
X is Element of the carrier of R
[X,x] is set
[X,F] is set
the InternalRel of R is V1() V4( the carrier of R) V5( the carrier of R) Element of K19(K20( the carrier of R, the carrier of R))
K20( the carrier of R, the carrier of R) is set
K19(K20( the carrier of R, the carrier of R)) is set
the InternalRel of S is V1() V4( the carrier of S) V5( the carrier of S) Element of K19(K20( the carrier of S, the carrier of S))
K20( the carrier of S, the carrier of S) is set
K19(K20( the carrier of S, the carrier of S)) is set
R is non empty RelStr
the carrier of R is non empty set
S is non empty RelStr
the carrier of S is non empty set
X is Element of the carrier of R
F is Element of the carrier of R
x is Element of the carrier of S
y is Element of the carrier of S
the carrier of R \/ the carrier of S is non empty set
(R,S) is non empty strict RelStr
the carrier of (R,S) is non empty set
z is Element of the carrier of (R,S)
a is Element of the carrier of (R,S)
R is non empty reflexive transitive antisymmetric with_suprema RelStr
the carrier of R is non empty set
K19( the carrier of R) is set
S is directed lower Element of K19( the carrier of R)
X is Element of the carrier of R
F is Element of the carrier of R
X "\/" F is Element of the carrier of R
x is Element of the carrier of R
R is RelStr
the carrier of R is set
S is RelStr
the carrier of S is set
the carrier of R /\ the carrier of S is set
K19( the carrier of R) is set
(R,S) is strict RelStr
the InternalRel of (R,S) is V1() V4( the carrier of (R,S)) V5( the carrier of (R,S)) Element of K19(K20( the carrier of (R,S), the carrier of (R,S)))
the carrier of (R,S) is set
K20( the carrier of (R,S), the carrier of (R,S)) is set
K19(K20( the carrier of (R,S), the carrier of (R,S))) is set
X is set
F is set
[X,F] is set
the InternalRel of R is V1() V4( the carrier of R) V5( the carrier of R) Element of K19(K20( the carrier of R, the carrier of R))
K20( the carrier of R, the carrier of R) is set
K19(K20( the carrier of R, the carrier of R)) is set
the InternalRel of S is V1() V4( the carrier of S) V5( the carrier of S) Element of K19(K20( the carrier of S, the carrier of S))
K20( the carrier of S, the carrier of S) is set
K19(K20( the carrier of S, the carrier of S)) is set
the InternalRel of R \/ the InternalRel of S is set
the InternalRel of R * the InternalRel of S is V1() V4( the carrier of R) V5( the carrier of S) Element of K19(K20( the carrier of R, the carrier of S))
K20( the carrier of R, the carrier of S) is set
K19(K20( the carrier of R, the carrier of S)) is set
( the InternalRel of R \/ the InternalRel of S) \/ ( the InternalRel of R * the InternalRel of S) is set
z is Element of the carrier of R
a is Element of the carrier of R
y is Element of K19( the carrier of R)
R is RelStr
S is RelStr
(R,S) is strict RelStr
the carrier of (R,S) is set
the carrier of R is set
the carrier of S is set
the carrier of R /\ the carrier of S is set
K19( the carrier of R) is set
X is Element of the carrier of (R,S)
F is Element of the carrier of (R,S)
[X,F] is set
the InternalRel of (R,S) is V1() V4( the carrier of (R,S)) V5( the carrier of (R,S)) Element of K19(K20( the carrier of (R,S), the carrier of (R,S)))
K20( the carrier of (R,S), the carrier of (R,S)) is set
K19(K20( the carrier of (R,S), the carrier of (R,S))) is set
R is non empty reflexive transitive antisymmetric with_suprema RelStr
the carrier of R is non empty set
S is non empty reflexive transitive antisymmetric with_suprema RelStr
the carrier of S is non empty set
the carrier of R /\ the carrier of S is set
K19( the carrier of S) is set
K19( the carrier of R) is set
X is Element of the carrier of R
F is Element of the carrier of R
X "\/" F is Element of the carrier of R
x is Element of the carrier of S
y is Element of the carrier of S
x "\/" y is Element of the carrier of S
z is Element of the carrier of R
a is Element of the carrier of R
(R,S) is non empty strict RelStr
the carrier of (R,S) is non empty set
X is Element of the carrier of (R,S)
D is Element of the carrier of (R,S)
dd is Element of the carrier of S
R is non empty reflexive transitive antisymmetric with_suprema lower-bounded RelStr
the carrier of R is non empty set
S is non empty reflexive transitive antisymmetric with_suprema lower-bounded RelStr
the carrier of S is non empty set
the carrier of R /\ the carrier of S is set
K19( the carrier of S) is set
Bottom S is Element of the carrier of S
X is set
F is Element of the carrier of S
R is RelStr
the carrier of R is set
S is RelStr
the carrier of S is set
the carrier of R /\ the carrier of S is set
K19( the carrier of S) is set
(R,S) is strict RelStr
the InternalRel of (R,S) is V1() V4( the carrier of (R,S)) V5( the carrier of (R,S)) Element of K19(K20( the carrier of (R,S), the carrier of (R,S)))
the carrier of (R,S) is set
K20( the carrier of (R,S), the carrier of (R,S)) is set
K19(K20( the carrier of (R,S), the carrier of (R,S))) is set
X is set
F is set
[X,F] is set
K19( the carrier of R) is set
the InternalRel of R is V1() V4( the carrier of R) V5( the carrier of R) Element of K19(K20( the carrier of R, the carrier of R))
K20( the carrier of R, the carrier of R) is set
K19(K20( the carrier of R, the carrier of R)) is set
the InternalRel of S is V1() V4( the carrier of S) V5( the carrier of S) Element of K19(K20( the carrier of S, the carrier of S))
K20( the carrier of S, the carrier of S) is set
K19(K20( the carrier of S, the carrier of S)) is set
the InternalRel of R \/ the InternalRel of S is set
the InternalRel of R * the InternalRel of S is V1() V4( the carrier of R) V5( the carrier of S) Element of K19(K20( the carrier of R, the carrier of S))
K20( the carrier of R, the carrier of S) is set
K19(K20( the carrier of R, the carrier of S)) is set
( the InternalRel of R \/ the InternalRel of S) \/ ( the InternalRel of R * the InternalRel of S) is set
z is Element of the carrier of S
a is Element of the carrier of S
y is Element of K19( the carrier of R)
R is set
S is set
[R,S] is set
X is RelStr
F is RelStr
(X,F) is strict RelStr
the InternalRel of (X,F) is V1() V4( the carrier of (X,F)) V5( the carrier of (X,F)) Element of K19(K20( the carrier of (X,F), the carrier of (X,F)))
the carrier of (X,F) is set
K20( the carrier of (X,F), the carrier of (X,F)) is set
K19(K20( the carrier of (X,F), the carrier of (X,F))) is set
the carrier of X is set
the carrier of F is set
the carrier of X /\ the carrier of F is set
K19( the carrier of X) is set
the carrier of X \ the carrier of F is Element of K19( the carrier of X)
the carrier of F \ the carrier of X is Element of K19( the carrier of F)
K19( the carrier of F) is set
the carrier of X \/ the carrier of F is set
R is RelStr
S is RelStr
(R,S) is strict RelStr
the carrier of (R,S) is set
the carrier of R is set
the carrier of S is set
the carrier of R /\ the carrier of S is set
K19( the carrier of S) is set
X is Element of the carrier of (R,S)
F is Element of the carrier of (R,S)
[X,F] is set
the InternalRel of (R,S) is V1() V4( the carrier of (R,S)) V5( the carrier of (R,S)) Element of K19(K20( the carrier of (R,S), the carrier of (R,S)))
K20( the carrier of (R,S), the carrier of (R,S)) is set
K19(K20( the carrier of (R,S), the carrier of (R,S))) is set
R is RelStr
S is RelStr
the carrier of R is set
the carrier of S is set
the carrier of R /\ the carrier of S is set
K19( the carrier of R) is set
K19( the carrier of S) is set
(R,S) is strict RelStr
the carrier of (R,S) is set
the InternalRel of (R,S) is V1() V4( the carrier of (R,S)) V5( the carrier of (R,S)) Element of K19(K20( the carrier of (R,S), the carrier of (R,S)))
K20( the carrier of (R,S), the carrier of (R,S)) is set
K19(K20( the carrier of (R,S), the carrier of (R,S))) is set
the InternalRel of S is V1() V4( the carrier of S) V5( the carrier of S) Element of K19(K20( the carrier of S, the carrier of S))
K20( the carrier of S, the carrier of S) is set
K19(K20( the carrier of S, the carrier of S)) is set
the InternalRel of R is V1() V4( the carrier of R) V5( the carrier of R) Element of K19(K20( the carrier of R, the carrier of R))
K20( the carrier of R, the carrier of R) is set
K19(K20( the carrier of R, the carrier of R)) is set
x is set
y is set
[x,y] is set
[y,x] is set
the carrier of R \/ the carrier of S is set
R is RelStr
the carrier of R is set
S is RelStr
the carrier of S is set
the carrier of R /\ the carrier of S is set
K19( the carrier of R) is set
K19( the carrier of S) is set
(R,S) is strict RelStr
the carrier of (R,S) is set
the InternalRel of (R,S) is V1() V4( the carrier of (R,S)) V5( the carrier of (R,S)) Element of K19(K20( the carrier of (R,S), the carrier of (R,S)))
K20( the carrier of (R,S), the carrier of (R,S)) is set
K19(K20( the carrier of (R,S), the carrier of (R,S))) is set
the InternalRel of S is V1() V4( the carrier of S) V5( the carrier of S) Element of K19(K20( the carrier of S, the carrier of S))
K20( the carrier of S, the carrier of S) is set
K19(K20( the carrier of S, the carrier of S)) is set
the InternalRel of R is V1() V4( the carrier of R) V5( the carrier of R) Element of K19(K20( the carrier of R, the carrier of R))
K20( the carrier of R, the carrier of R) is set
K19(K20( the carrier of R, the carrier of R)) is set
x is set
y is set
z is set
[x,y] is set
[y,z] is set
[x,z] is set
the carrier of R \/ the carrier of S is set
the InternalRel of R \/ the InternalRel of S is set
the InternalRel of R * the InternalRel of S is V1() V4( the carrier of R) V5( the carrier of S) Element of K19(K20( the carrier of R, the carrier of S))
K20( the carrier of R, the carrier of S) is set
K19(K20( the carrier of R, the carrier of S)) is set
( the InternalRel of R \/ the InternalRel of S) \/ ( the InternalRel of R * the InternalRel of S) is set
a is set
[y,a] is set
[a,z] is set
[x,a] is set
the InternalRel of R \/ the InternalRel of S is set
the InternalRel of R * the InternalRel of S is V1() V4( the carrier of R) V5( the carrier of S) Element of K19(K20( the carrier of R, the carrier of S))
K20( the carrier of R, the carrier of S) is set
K19(K20( the carrier of R, the carrier of S)) is set
( the InternalRel of R \/ the InternalRel of S) \/ ( the InternalRel of R * the InternalRel of S) is set
a is set
[x,a] is set
[a,y] is set
[a,z] is set