:: 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