:: LATSUM_1 semantic presentation

begin

theorem :: LATSUM_1:1
for x, y, A, B being ( ( ) ( ) set ) st x : ( ( ) ( ) set ) in A : ( ( ) ( ) set ) \/ B : ( ( ) ( ) set ) : ( ( ) ( ) set ) & y : ( ( ) ( ) set ) in A : ( ( ) ( ) set ) \/ B : ( ( ) ( ) set ) : ( ( ) ( ) set ) & not ( x : ( ( ) ( ) set ) in A : ( ( ) ( ) set ) \ B : ( ( ) ( ) set ) : ( ( ) ( ) Element of K19(b3 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) & y : ( ( ) ( ) set ) in A : ( ( ) ( ) set ) \ B : ( ( ) ( ) set ) : ( ( ) ( ) Element of K19(b3 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) & not ( x : ( ( ) ( ) set ) in B : ( ( ) ( ) set ) & y : ( ( ) ( ) set ) in B : ( ( ) ( ) set ) ) & not ( x : ( ( ) ( ) set ) in A : ( ( ) ( ) set ) \ B : ( ( ) ( ) set ) : ( ( ) ( ) Element of K19(b3 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) & y : ( ( ) ( ) set ) in B : ( ( ) ( ) set ) ) holds
( x : ( ( ) ( ) set ) in B : ( ( ) ( ) set ) & y : ( ( ) ( ) set ) in A : ( ( ) ( ) set ) \ B : ( ( ) ( ) set ) : ( ( ) ( ) Element of K19(b3 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ;

definition
let R, S be ( ( ) ( ) RelStr ) ;
pred R tolerates S means :: LATSUM_1:def 1
 for x, y being ( ( ) ( ) set ) st x : ( ( ) ( ) set ) in the carrier of R : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) /\ the carrier of S : ( ( ) ( ) NetStr over R : ( ( ) ( ) 1-sorted ) ) : ( ( ) ( ) set ) : ( ( ) ( ) set ) & y : ( ( ) ( ) set ) in the carrier of R : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) /\ the carrier of S : ( ( ) ( ) NetStr over R : ( ( ) ( ) 1-sorted ) ) : ( ( ) ( ) set ) : ( ( ) ( ) set ) holds
( [x : ( ( ) ( ) set ) ,y : ( ( ) ( ) set ) ] : ( ( ) ( ) set ) in the InternalRel of R : ( ( ) ( ) 1-sorted ) : ( ( ) ( V1() V4( the carrier of R : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) ) V5( the carrier of R : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) ) ) Element of K19(K20( the carrier of R : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) , the carrier of R : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) iff [x : ( ( ) ( ) set ) ,y : ( ( ) ( ) set ) ] : ( ( ) ( ) set ) in the InternalRel of S : ( ( ) ( ) NetStr over R : ( ( ) ( ) 1-sorted ) ) : ( ( ) ( V1() V4( the carrier of S : ( ( ) ( ) NetStr over R : ( ( ) ( ) 1-sorted ) ) : ( ( ) ( ) set ) ) V5( the carrier of S : ( ( ) ( ) NetStr over R : ( ( ) ( ) 1-sorted ) ) : ( ( ) ( ) set ) ) ) Element of K19(K20( the carrier of S : ( ( ) ( ) NetStr over R : ( ( ) ( ) 1-sorted ) ) : ( ( ) ( ) set ) , the carrier of S : ( ( ) ( ) NetStr over R : ( ( ) ( ) 1-sorted ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) );
end;

begin

definition
let R, S be ( ( ) ( ) RelStr ) ;
func R [*] S -> ( ( strict ) ( strict ) RelStr ) means :: LATSUM_1:def 2
( the carrier of it : ( ( ) ( V1() V4(S : ( ( ) ( ) NetStr over R : ( ( ) ( ) 1-sorted ) ) ) V5(S : ( ( ) ( ) NetStr over R : ( ( ) ( ) 1-sorted ) ) ) ) Element of K19(K20(S : ( ( ) ( ) NetStr over R : ( ( ) ( ) 1-sorted ) ) ,S : ( ( ) ( ) NetStr over R : ( ( ) ( ) 1-sorted ) ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) = the carrier of R : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) \/ the carrier of S : ( ( ) ( ) NetStr over R : ( ( ) ( ) 1-sorted ) ) : ( ( ) ( ) set ) : ( ( ) ( ) set ) & the InternalRel of it : ( ( ) ( V1() V4(S : ( ( ) ( ) NetStr over R : ( ( ) ( ) 1-sorted ) ) ) V5(S : ( ( ) ( ) NetStr over R : ( ( ) ( ) 1-sorted ) ) ) ) Element of K19(K20(S : ( ( ) ( ) NetStr over R : ( ( ) ( ) 1-sorted ) ) ,S : ( ( ) ( ) NetStr over R : ( ( ) ( ) 1-sorted ) ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( V1() V4( the carrier of it : ( ( ) ( V1() V4(S : ( ( ) ( ) NetStr over R : ( ( ) ( ) 1-sorted ) ) ) V5(S : ( ( ) ( ) NetStr over R : ( ( ) ( ) 1-sorted ) ) ) ) Element of K19(K20(S : ( ( ) ( ) NetStr over R : ( ( ) ( ) 1-sorted ) ) ,S : ( ( ) ( ) NetStr over R : ( ( ) ( ) 1-sorted ) ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) V5( the carrier of it : ( ( ) ( V1() V4(S : ( ( ) ( ) NetStr over R : ( ( ) ( ) 1-sorted ) ) ) V5(S : ( ( ) ( ) NetStr over R : ( ( ) ( ) 1-sorted ) ) ) ) Element of K19(K20(S : ( ( ) ( ) NetStr over R : ( ( ) ( ) 1-sorted ) ) ,S : ( ( ) ( ) NetStr over R : ( ( ) ( ) 1-sorted ) ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) Element of K19(K20( the carrier of it : ( ( ) ( V1() V4(S : ( ( ) ( ) NetStr over R : ( ( ) ( ) 1-sorted ) ) ) V5(S : ( ( ) ( ) NetStr over R : ( ( ) ( ) 1-sorted ) ) ) ) Element of K19(K20(S : ( ( ) ( ) NetStr over R : ( ( ) ( ) 1-sorted ) ) ,S : ( ( ) ( ) NetStr over R : ( ( ) ( ) 1-sorted ) ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) , the carrier of it : ( ( ) ( V1() V4(S : ( ( ) ( ) NetStr over R : ( ( ) ( ) 1-sorted ) ) ) V5(S : ( ( ) ( ) NetStr over R : ( ( ) ( ) 1-sorted ) ) ) ) Element of K19(K20(S : ( ( ) ( ) NetStr over R : ( ( ) ( ) 1-sorted ) ) ,S : ( ( ) ( ) NetStr over R : ( ( ) ( ) 1-sorted ) ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) = ( the InternalRel of R : ( ( ) ( ) 1-sorted ) : ( ( ) ( V1() V4( the carrier of R : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) ) V5( the carrier of R : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) ) ) Element of K19(K20( the carrier of R : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) , the carrier of R : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) \/ the InternalRel of S : ( ( ) ( ) NetStr over R : ( ( ) ( ) 1-sorted ) ) : ( ( ) ( V1() V4( the carrier of S : ( ( ) ( ) NetStr over R : ( ( ) ( ) 1-sorted ) ) : ( ( ) ( ) set ) ) V5( the carrier of S : ( ( ) ( ) NetStr over R : ( ( ) ( ) 1-sorted ) ) : ( ( ) ( ) set ) ) ) Element of K19(K20( the carrier of S : ( ( ) ( ) NetStr over R : ( ( ) ( ) 1-sorted ) ) : ( ( ) ( ) set ) , the carrier of S : ( ( ) ( ) NetStr over R : ( ( ) ( ) 1-sorted ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ) set ) \/ ( the InternalRel of R : ( ( ) ( ) 1-sorted ) : ( ( ) ( V1() V4( the carrier of R : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) ) V5( the carrier of R : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) ) ) Element of K19(K20( the carrier of R : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) , the carrier of R : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) * the InternalRel of S : ( ( ) ( ) NetStr over R : ( ( ) ( ) 1-sorted ) ) : ( ( ) ( V1() V4( the carrier of S : ( ( ) ( ) NetStr over R : ( ( ) ( ) 1-sorted ) ) : ( ( ) ( ) set ) ) V5( the carrier of S : ( ( ) ( ) NetStr over R : ( ( ) ( ) 1-sorted ) ) : ( ( ) ( ) set ) ) ) Element of K19(K20( the carrier of S : ( ( ) ( ) NetStr over R : ( ( ) ( ) 1-sorted ) ) : ( ( ) ( ) set ) , the carrier of S : ( ( ) ( ) NetStr over R : ( ( ) ( ) 1-sorted ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V1() V4( the carrier of R : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) ) V5( the carrier of S : ( ( ) ( ) NetStr over R : ( ( ) ( ) 1-sorted ) ) : ( ( ) ( ) set ) ) ) Element of K19(K20( the carrier of R : ( ( ) ( ) 1-sorted ) : ( ( ) ( ) set ) , the carrier of S : ( ( ) ( ) NetStr over R : ( ( ) ( ) 1-sorted ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) );
end;

registration
let R be ( ( ) ( ) RelStr ) ;
let S be ( ( non empty ) ( non empty ) RelStr ) ;
cluster R : ( ( ) ( ) RelStr ) [*] S : ( ( non empty ) ( non empty ) RelStr ) : ( ( strict ) ( strict ) RelStr ) -> non empty strict ;
end;

registration
let R be ( ( non empty ) ( non empty ) RelStr ) ;
let S be ( ( ) ( ) RelStr ) ;
cluster R : ( ( non empty ) ( non empty ) RelStr ) [*] S : ( ( ) ( ) RelStr ) : ( ( strict ) ( strict ) RelStr ) -> non empty strict ;
end;

theorem :: LATSUM_1:2
for R, S being ( ( ) ( ) RelStr ) holds
( the InternalRel of R : ( ( ) ( ) RelStr ) : ( ( ) ( V1() V4( the carrier of b1 : ( ( ) ( ) RelStr ) : ( ( ) ( ) set ) ) V5( the carrier of b1 : ( ( ) ( ) RelStr ) : ( ( ) ( ) set ) ) ) Element of K19(K20( the carrier of b1 : ( ( ) ( ) RelStr ) : ( ( ) ( ) set ) , the carrier of b1 : ( ( ) ( ) RelStr ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) c= the InternalRel of (R : ( ( ) ( ) RelStr ) [*] S : ( ( ) ( ) RelStr ) ) : ( ( strict ) ( strict ) RelStr ) : ( ( ) ( V1() V4( the carrier of (b1 : ( ( ) ( ) RelStr ) [*] b2 : ( ( ) ( ) RelStr ) ) : ( ( strict ) ( strict ) RelStr ) : ( ( ) ( ) set ) ) V5( the carrier of (b1 : ( ( ) ( ) RelStr ) [*] b2 : ( ( ) ( ) RelStr ) ) : ( ( strict ) ( strict ) RelStr ) : ( ( ) ( ) set ) ) ) Element of K19(K20( the carrier of (b1 : ( ( ) ( ) RelStr ) [*] b2 : ( ( ) ( ) RelStr ) ) : ( ( strict ) ( strict ) RelStr ) : ( ( ) ( ) set ) , the carrier of (b1 : ( ( ) ( ) RelStr ) [*] b2 : ( ( ) ( ) RelStr ) ) : ( ( strict ) ( strict ) RelStr ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) & the InternalRel of S : ( ( ) ( ) RelStr ) : ( ( ) ( V1() V4( the carrier of b2 : ( ( ) ( ) RelStr ) : ( ( ) ( ) set ) ) V5( the carrier of b2 : ( ( ) ( ) RelStr ) : ( ( ) ( ) set ) ) ) Element of K19(K20( the carrier of b2 : ( ( ) ( ) RelStr ) : ( ( ) ( ) set ) , the carrier of b2 : ( ( ) ( ) RelStr ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) c= the InternalRel of (R : ( ( ) ( ) RelStr ) [*] S : ( ( ) ( ) RelStr ) ) : ( ( strict ) ( strict ) RelStr ) : ( ( ) ( V1() V4( the carrier of (b1 : ( ( ) ( ) RelStr ) [*] b2 : ( ( ) ( ) RelStr ) ) : ( ( strict ) ( strict ) RelStr ) : ( ( ) ( ) set ) ) V5( the carrier of (b1 : ( ( ) ( ) RelStr ) [*] b2 : ( ( ) ( ) RelStr ) ) : ( ( strict ) ( strict ) RelStr ) : ( ( ) ( ) set ) ) ) Element of K19(K20( the carrier of (b1 : ( ( ) ( ) RelStr ) [*] b2 : ( ( ) ( ) RelStr ) ) : ( ( strict ) ( strict ) RelStr ) : ( ( ) ( ) set ) , the carrier of (b1 : ( ( ) ( ) RelStr ) [*] b2 : ( ( ) ( ) RelStr ) ) : ( ( strict ) ( strict ) RelStr ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ;

theorem :: LATSUM_1:3
for R, S being ( ( ) ( ) RelStr ) st R : ( ( ) ( ) RelStr ) is reflexive & S : ( ( ) ( ) RelStr ) is reflexive holds
R : ( ( ) ( ) RelStr ) [*] S : ( ( ) ( ) RelStr ) : ( ( strict ) ( strict ) RelStr ) is reflexive ;

begin

theorem :: LATSUM_1:4
for R, S being ( ( ) ( ) RelStr )
for a, b being ( ( ) ( ) set ) st [a : ( ( ) ( ) set ) ,b : ( ( ) ( ) set ) ] : ( ( ) ( ) set ) in the InternalRel of (R : ( ( ) ( ) RelStr ) [*] S : ( ( ) ( ) RelStr ) ) : ( ( strict ) ( strict ) RelStr ) : ( ( ) ( V1() V4( the carrier of (b1 : ( ( ) ( ) RelStr ) [*] b2 : ( ( ) ( ) RelStr ) ) : ( ( strict ) ( strict ) RelStr ) : ( ( ) ( ) set ) ) V5( the carrier of (b1 : ( ( ) ( ) RelStr ) [*] b2 : ( ( ) ( ) RelStr ) ) : ( ( strict ) ( strict ) RelStr ) : ( ( ) ( ) set ) ) ) Element of K19(K20( the carrier of (b1 : ( ( ) ( ) RelStr ) [*] b2 : ( ( ) ( ) RelStr ) ) : ( ( strict ) ( strict ) RelStr ) : ( ( ) ( ) set ) , the carrier of (b1 : ( ( ) ( ) RelStr ) [*] b2 : ( ( ) ( ) RelStr ) ) : ( ( strict ) ( strict ) RelStr ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) & a : ( ( ) ( ) set ) in the carrier of R : ( ( ) ( ) RelStr ) : ( ( ) ( ) set ) & b : ( ( ) ( ) set ) in the carrier of R : ( ( ) ( ) RelStr ) : ( ( ) ( ) set ) & R : ( ( ) ( ) RelStr ) tolerates S : ( ( ) ( ) RelStr ) & R : ( ( ) ( ) RelStr ) is transitive holds
[a : ( ( ) ( ) set ) ,b : ( ( ) ( ) set ) ] : ( ( ) ( ) set ) in the InternalRel of R : ( ( ) ( ) RelStr ) : ( ( ) ( V1() V4( the carrier of b1 : ( ( ) ( ) RelStr ) : ( ( ) ( ) set ) ) V5( the carrier of b1 : ( ( ) ( ) RelStr ) : ( ( ) ( ) set ) ) ) Element of K19(K20( the carrier of b1 : ( ( ) ( ) RelStr ) : ( ( ) ( ) set ) , the carrier of b1 : ( ( ) ( ) RelStr ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ;

theorem :: LATSUM_1:5
for R, S being ( ( ) ( ) RelStr )
for a, b being ( ( ) ( ) set ) st [a : ( ( ) ( ) set ) ,b : ( ( ) ( ) set ) ] : ( ( ) ( ) set ) in the InternalRel of (R : ( ( ) ( ) RelStr ) [*] S : ( ( ) ( ) RelStr ) ) : ( ( strict ) ( strict ) RelStr ) : ( ( ) ( V1() V4( the carrier of (b1 : ( ( ) ( ) RelStr ) [*] b2 : ( ( ) ( ) RelStr ) ) : ( ( strict ) ( strict ) RelStr ) : ( ( ) ( ) set ) ) V5( the carrier of (b1 : ( ( ) ( ) RelStr ) [*] b2 : ( ( ) ( ) RelStr ) ) : ( ( strict ) ( strict ) RelStr ) : ( ( ) ( ) set ) ) ) Element of K19(K20( the carrier of (b1 : ( ( ) ( ) RelStr ) [*] b2 : ( ( ) ( ) RelStr ) ) : ( ( strict ) ( strict ) RelStr ) : ( ( ) ( ) set ) , the carrier of (b1 : ( ( ) ( ) RelStr ) [*] b2 : ( ( ) ( ) RelStr ) ) : ( ( strict ) ( strict ) RelStr ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) & a : ( ( ) ( ) set ) in the carrier of S : ( ( ) ( ) RelStr ) : ( ( ) ( ) set ) & b : ( ( ) ( ) set ) in the carrier of S : ( ( ) ( ) RelStr ) : ( ( ) ( ) set ) & R : ( ( ) ( ) RelStr ) tolerates S : ( ( ) ( ) RelStr ) & S : ( ( ) ( ) RelStr ) is transitive holds
[a : ( ( ) ( ) set ) ,b : ( ( ) ( ) set ) ] : ( ( ) ( ) set ) in the InternalRel of S : ( ( ) ( ) RelStr ) : ( ( ) ( V1() V4( the carrier of b2 : ( ( ) ( ) RelStr ) : ( ( ) ( ) set ) ) V5( the carrier of b2 : ( ( ) ( ) RelStr ) : ( ( ) ( ) set ) ) ) Element of K19(K20( the carrier of b2 : ( ( ) ( ) RelStr ) : ( ( ) ( ) set ) , the carrier of b2 : ( ( ) ( ) RelStr ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ;

theorem :: LATSUM_1:6
for R, S being ( ( ) ( ) RelStr )
for a, b being ( ( ) ( ) set ) holds
( ( [a : ( ( ) ( ) set ) ,b : ( ( ) ( ) set ) ] : ( ( ) ( ) set ) in the InternalRel of R : ( ( ) ( ) RelStr ) : ( ( ) ( V1() V4( the carrier of b1 : ( ( ) ( ) RelStr ) : ( ( ) ( ) set ) ) V5( the carrier of b1 : ( ( ) ( ) RelStr ) : ( ( ) ( ) set ) ) ) Element of K19(K20( the carrier of b1 : ( ( ) ( ) RelStr ) : ( ( ) ( ) set ) , the carrier of b1 : ( ( ) ( ) RelStr ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) implies [a : ( ( ) ( ) set ) ,b : ( ( ) ( ) set ) ] : ( ( ) ( ) set ) in the InternalRel of (R : ( ( ) ( ) RelStr ) [*] S : ( ( ) ( ) RelStr ) ) : ( ( strict ) ( strict ) RelStr ) : ( ( ) ( V1() V4( the carrier of (b1 : ( ( ) ( ) RelStr ) [*] b2 : ( ( ) ( ) RelStr ) ) : ( ( strict ) ( strict ) RelStr ) : ( ( ) ( ) set ) ) V5( the carrier of (b1 : ( ( ) ( ) RelStr ) [*] b2 : ( ( ) ( ) RelStr ) ) : ( ( strict ) ( strict ) RelStr ) : ( ( ) ( ) set ) ) ) Element of K19(K20( the carrier of (b1 : ( ( ) ( ) RelStr ) [*] b2 : ( ( ) ( ) RelStr ) ) : ( ( strict ) ( strict ) RelStr ) : ( ( ) ( ) set ) , the carrier of (b1 : ( ( ) ( ) RelStr ) [*] b2 : ( ( ) ( ) RelStr ) ) : ( ( strict ) ( strict ) RelStr ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) & ( [a : ( ( ) ( ) set ) ,b : ( ( ) ( ) set ) ] : ( ( ) ( ) set ) in the InternalRel of S : ( ( ) ( ) RelStr ) : ( ( ) ( V1() V4( the carrier of b2 : ( ( ) ( ) RelStr ) : ( ( ) ( ) set ) ) V5( the carrier of b2 : ( ( ) ( ) RelStr ) : ( ( ) ( ) set ) ) ) Element of K19(K20( the carrier of b2 : ( ( ) ( ) RelStr ) : ( ( ) ( ) set ) , the carrier of b2 : ( ( ) ( ) RelStr ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) implies [a : ( ( ) ( ) set ) ,b : ( ( ) ( ) set ) ] : ( ( ) ( ) set ) in the InternalRel of (R : ( ( ) ( ) RelStr ) [*] S : ( ( ) ( ) RelStr ) ) : ( ( strict ) ( strict ) RelStr ) : ( ( ) ( V1() V4( the carrier of (b1 : ( ( ) ( ) RelStr ) [*] b2 : ( ( ) ( ) RelStr ) ) : ( ( strict ) ( strict ) RelStr ) : ( ( ) ( ) set ) ) V5( the carrier of (b1 : ( ( ) ( ) RelStr ) [*] b2 : ( ( ) ( ) RelStr ) ) : ( ( strict ) ( strict ) RelStr ) : ( ( ) ( ) set ) ) ) Element of K19(K20( the carrier of (b1 : ( ( ) ( ) RelStr ) [*] b2 : ( ( ) ( ) RelStr ) ) : ( ( strict ) ( strict ) RelStr ) : ( ( ) ( ) set ) , the carrier of (b1 : ( ( ) ( ) RelStr ) [*] b2 : ( ( ) ( ) RelStr ) ) : ( ( strict ) ( strict ) RelStr ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) ;

theorem :: LATSUM_1:7
for R, S being ( ( non empty ) ( non empty ) RelStr )
for x being ( ( ) ( ) Element of ( ( ) ( ) set ) ) holds
( x : ( ( ) ( ) Element of ( ( ) ( ) set ) ) in the carrier of R : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) or x : ( ( ) ( ) Element of ( ( ) ( ) set ) ) in the carrier of S : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) \ the carrier of R : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) : ( ( ) ( ) Element of K19( the carrier of b2 : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) ;

theorem :: LATSUM_1:8
for R, S being ( ( non empty ) ( non empty ) RelStr )
for x, y being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) )
for a, b being ( ( ) ( ) Element of ( ( ) ( ) set ) ) st x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) = a : ( ( ) ( ) Element of ( ( ) ( ) set ) ) & y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) = b : ( ( ) ( ) Element of ( ( ) ( ) set ) ) & R : ( ( non empty ) ( non empty ) RelStr ) tolerates S : ( ( non empty ) ( non empty ) RelStr ) & R : ( ( non empty ) ( non empty ) RelStr ) is transitive holds
( x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) <= y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) iff a : ( ( ) ( ) Element of ( ( ) ( ) set ) ) <= b : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ) ;

theorem :: LATSUM_1:9
for R, S being ( ( non empty ) ( non empty ) RelStr )
for a, b being ( ( ) ( ) Element of ( ( ) ( ) set ) )
for c, d being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) st a : ( ( ) ( ) Element of ( ( ) ( ) set ) ) = c : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) & b : ( ( ) ( ) Element of ( ( ) ( ) set ) ) = d : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) & R : ( ( non empty ) ( non empty ) RelStr ) tolerates S : ( ( non empty ) ( non empty ) RelStr ) & S : ( ( non empty ) ( non empty ) RelStr ) is transitive holds
( a : ( ( ) ( ) Element of ( ( ) ( ) set ) ) <= b : ( ( ) ( ) Element of ( ( ) ( ) set ) ) iff c : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) <= d : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) ;

theorem :: LATSUM_1:10
for R, S being ( ( non empty reflexive transitive antisymmetric with_suprema ) ( non empty reflexive transitive antisymmetric with_suprema ) RelStr )
for x being ( ( ) ( ) set ) st x : ( ( ) ( ) set ) in the carrier of R : ( ( non empty reflexive transitive antisymmetric with_suprema ) ( non empty reflexive transitive antisymmetric with_suprema ) RelStr ) : ( ( ) ( non empty ) set ) holds
x : ( ( ) ( ) set ) is ( ( ) ( ) Element of ( ( ) ( ) set ) ) ;

theorem :: LATSUM_1:11
for R, S being ( ( non empty reflexive transitive antisymmetric with_suprema ) ( non empty reflexive transitive antisymmetric with_suprema ) RelStr )
for x being ( ( ) ( ) set ) st x : ( ( ) ( ) set ) in the carrier of S : ( ( non empty reflexive transitive antisymmetric with_suprema ) ( non empty reflexive transitive antisymmetric with_suprema ) RelStr ) : ( ( ) ( non empty ) set ) holds
x : ( ( ) ( ) set ) is ( ( ) ( ) Element of ( ( ) ( ) set ) ) ;

theorem :: LATSUM_1:12
for R, S being ( ( non empty ) ( non empty ) RelStr )
for x being ( ( ) ( ) set ) st x : ( ( ) ( ) set ) in the carrier of R : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) /\ the carrier of S : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) : ( ( ) ( ) set ) holds
x : ( ( ) ( ) set ) is ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ;

theorem :: LATSUM_1:13
for R, S being ( ( non empty ) ( non empty ) RelStr )
for x being ( ( ) ( ) set ) st x : ( ( ) ( ) set ) in the carrier of R : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) /\ the carrier of S : ( ( non empty ) ( non empty ) RelStr ) : ( ( ) ( non empty ) set ) : ( ( ) ( ) set ) holds
x : ( ( ) ( ) set ) is ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ;

theorem :: LATSUM_1:14
for R, S being ( ( non empty reflexive transitive antisymmetric with_suprema ) ( non empty reflexive transitive antisymmetric with_suprema ) RelStr )
for x, y being ( ( ) ( ) Element of ( ( ) ( ) set ) ) st x : ( ( ) ( ) Element of ( ( ) ( ) set ) ) in the carrier of R : ( ( non empty reflexive transitive antisymmetric with_suprema ) ( non empty reflexive transitive antisymmetric with_suprema ) RelStr ) : ( ( ) ( non empty ) set ) & y : ( ( ) ( ) Element of ( ( ) ( ) set ) ) in the carrier of S : ( ( non empty reflexive transitive antisymmetric with_suprema ) ( non empty reflexive transitive antisymmetric with_suprema ) RelStr ) : ( ( ) ( non empty ) set ) & R : ( ( non empty reflexive transitive antisymmetric with_suprema ) ( non empty reflexive transitive antisymmetric with_suprema ) RelStr ) tolerates S : ( ( non empty reflexive transitive antisymmetric with_suprema ) ( non empty reflexive transitive antisymmetric with_suprema ) RelStr ) holds
( x : ( ( ) ( ) Element of ( ( ) ( ) set ) ) <= y : ( ( ) ( ) Element of ( ( ) ( ) set ) ) iff ex a being ( ( ) ( ) Element of ( ( ) ( ) set ) ) st
( a : ( ( ) ( ) Element of ( ( ) ( ) set ) ) in the carrier of R : ( ( non empty reflexive transitive antisymmetric with_suprema ) ( non empty reflexive transitive antisymmetric with_suprema ) RelStr ) : ( ( ) ( non empty ) set ) /\ the carrier of S : ( ( non empty reflexive transitive antisymmetric with_suprema ) ( non empty reflexive transitive antisymmetric with_suprema ) RelStr ) : ( ( ) ( non empty ) set ) : ( ( ) ( ) set ) & x : ( ( ) ( ) Element of ( ( ) ( ) set ) ) <= a : ( ( ) ( ) Element of ( ( ) ( ) set ) ) & a : ( ( ) ( ) Element of ( ( ) ( ) set ) ) <= y : ( ( ) ( ) Element of ( ( ) ( ) set ) ) ) ) ;

theorem :: LATSUM_1:15
for R, S being ( ( non empty ) ( non empty ) RelStr )
for a, b being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) )
for c, d being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) st a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) = c : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) & b : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) = d : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) & R : ( ( non empty ) ( non empty ) RelStr ) tolerates S : ( ( non empty ) ( non empty ) RelStr ) & R : ( ( non empty ) ( non empty ) RelStr ) is transitive & S : ( ( non empty ) ( non empty ) RelStr ) is transitive holds
( a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) <= b : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) iff c : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) <= d : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) ) ;

theorem :: LATSUM_1:16
for R being ( ( non empty reflexive transitive antisymmetric with_suprema ) ( non empty reflexive transitive antisymmetric with_suprema ) RelStr )
for D being ( ( directed lower ) ( directed lower ) Subset of )
for x, y being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) st x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) in D : ( ( directed lower ) ( directed lower ) Subset of ) & y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) in D : ( ( directed lower ) ( directed lower ) Subset of ) holds
x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) "\/" y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty reflexive transitive antisymmetric with_suprema ) ( non empty reflexive transitive antisymmetric with_suprema ) RelStr ) : ( ( ) ( non empty ) set ) ) in D : ( ( directed lower ) ( directed lower ) Subset of ) ;

theorem :: LATSUM_1:17
for R, S being ( ( ) ( ) RelStr )
for a, b being ( ( ) ( ) set ) st the carrier of R : ( ( ) ( ) RelStr ) : ( ( ) ( ) set ) /\ the carrier of S : ( ( ) ( ) RelStr ) : ( ( ) ( ) set ) : ( ( ) ( ) set ) is ( ( upper ) ( upper ) Subset of ) & [a : ( ( ) ( ) set ) ,b : ( ( ) ( ) set ) ] : ( ( ) ( ) set ) in the InternalRel of (R : ( ( ) ( ) RelStr ) [*] S : ( ( ) ( ) RelStr ) ) : ( ( strict ) ( strict ) RelStr ) : ( ( ) ( V1() V4( the carrier of (b1 : ( ( ) ( ) RelStr ) [*] b2 : ( ( ) ( ) RelStr ) ) : ( ( strict ) ( strict ) RelStr ) : ( ( ) ( ) set ) ) V5( the carrier of (b1 : ( ( ) ( ) RelStr ) [*] b2 : ( ( ) ( ) RelStr ) ) : ( ( strict ) ( strict ) RelStr ) : ( ( ) ( ) set ) ) ) Element of K19(K20( the carrier of (b1 : ( ( ) ( ) RelStr ) [*] b2 : ( ( ) ( ) RelStr ) ) : ( ( strict ) ( strict ) RelStr ) : ( ( ) ( ) set ) , the carrier of (b1 : ( ( ) ( ) RelStr ) [*] b2 : ( ( ) ( ) RelStr ) ) : ( ( strict ) ( strict ) RelStr ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) & a : ( ( ) ( ) set ) in the carrier of S : ( ( ) ( ) RelStr ) : ( ( ) ( ) set ) holds
b : ( ( ) ( ) set ) in the carrier of S : ( ( ) ( ) RelStr ) : ( ( ) ( ) set ) ;

theorem :: LATSUM_1:18
for R, S being ( ( ) ( ) RelStr )
for a, b being ( ( ) ( ) Element of ( ( ) ( ) set ) ) st the carrier of R : ( ( ) ( ) RelStr ) : ( ( ) ( ) set ) /\ the carrier of S : ( ( ) ( ) RelStr ) : ( ( ) ( ) set ) : ( ( ) ( ) set ) is ( ( upper ) ( upper ) Subset of ) & a : ( ( ) ( ) Element of ( ( ) ( ) set ) ) <= b : ( ( ) ( ) Element of ( ( ) ( ) set ) ) & a : ( ( ) ( ) Element of ( ( ) ( ) set ) ) in the carrier of S : ( ( ) ( ) RelStr ) : ( ( ) ( ) set ) holds
b : ( ( ) ( ) Element of ( ( ) ( ) set ) ) in the carrier of S : ( ( ) ( ) RelStr ) : ( ( ) ( ) set ) ;

theorem :: LATSUM_1:19
for R, S being ( ( non empty reflexive transitive antisymmetric with_suprema ) ( non empty reflexive transitive antisymmetric with_suprema ) RelStr )
for x, y being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) )
for a, b being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) st the carrier of R : ( ( non empty reflexive transitive antisymmetric with_suprema ) ( non empty reflexive transitive antisymmetric with_suprema ) RelStr ) : ( ( ) ( non empty ) set ) /\ the carrier of S : ( ( non empty reflexive transitive antisymmetric with_suprema ) ( non empty reflexive transitive antisymmetric with_suprema ) RelStr ) : ( ( ) ( non empty ) set ) : ( ( ) ( ) set ) is ( ( directed lower ) ( directed lower ) Subset of ) & the carrier of R : ( ( non empty reflexive transitive antisymmetric with_suprema ) ( non empty reflexive transitive antisymmetric with_suprema ) RelStr ) : ( ( ) ( non empty ) set ) /\ the carrier of S : ( ( non empty reflexive transitive antisymmetric with_suprema ) ( non empty reflexive transitive antisymmetric with_suprema ) RelStr ) : ( ( ) ( non empty ) set ) : ( ( ) ( ) set ) is ( ( upper ) ( upper ) Subset of ) & R : ( ( non empty reflexive transitive antisymmetric with_suprema ) ( non empty reflexive transitive antisymmetric with_suprema ) RelStr ) tolerates S : ( ( non empty reflexive transitive antisymmetric with_suprema ) ( non empty reflexive transitive antisymmetric with_suprema ) RelStr ) & x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) = a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) & y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) = b : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds
x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) "\/" y : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty reflexive transitive antisymmetric with_suprema ) ( non empty reflexive transitive antisymmetric with_suprema ) RelStr ) : ( ( ) ( non empty ) set ) ) = a : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) "\/" b : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of b2 : ( ( non empty reflexive transitive antisymmetric with_suprema ) ( non empty reflexive transitive antisymmetric with_suprema ) RelStr ) : ( ( ) ( non empty ) set ) ) ;

theorem :: LATSUM_1:20
for R, S being ( ( non empty reflexive transitive antisymmetric with_suprema lower-bounded ) ( non empty reflexive transitive antisymmetric with_suprema lower-bounded ) RelStr ) st the carrier of R : ( ( non empty reflexive transitive antisymmetric with_suprema lower-bounded ) ( non empty reflexive transitive antisymmetric with_suprema lower-bounded ) RelStr ) : ( ( ) ( non empty ) set ) /\ the carrier of S : ( ( non empty reflexive transitive antisymmetric with_suprema lower-bounded ) ( non empty reflexive transitive antisymmetric with_suprema lower-bounded ) RelStr ) : ( ( ) ( non empty ) set ) : ( ( ) ( ) set ) is ( ( non empty directed lower ) ( non empty directed lower ) Subset of ) holds
Bottom S : ( ( non empty reflexive transitive antisymmetric with_suprema lower-bounded ) ( non empty reflexive transitive antisymmetric with_suprema lower-bounded ) RelStr ) : ( ( ) ( ) Element of the carrier of b2 : ( ( non empty reflexive transitive antisymmetric with_suprema lower-bounded ) ( non empty reflexive transitive antisymmetric with_suprema lower-bounded ) RelStr ) : ( ( ) ( non empty ) set ) ) in the carrier of R : ( ( non empty reflexive transitive antisymmetric with_suprema lower-bounded ) ( non empty reflexive transitive antisymmetric with_suprema lower-bounded ) RelStr ) : ( ( ) ( non empty ) set ) ;

theorem :: LATSUM_1:21
for R, S being ( ( ) ( ) RelStr )
for a, b being ( ( ) ( ) set ) st the carrier of R : ( ( ) ( ) RelStr ) : ( ( ) ( ) set ) /\ the carrier of S : ( ( ) ( ) RelStr ) : ( ( ) ( ) set ) : ( ( ) ( ) set ) is ( ( lower ) ( lower ) Subset of ) & [a : ( ( ) ( ) set ) ,b : ( ( ) ( ) set ) ] : ( ( ) ( ) set ) in the InternalRel of (R : ( ( ) ( ) RelStr ) [*] S : ( ( ) ( ) RelStr ) ) : ( ( strict ) ( strict ) RelStr ) : ( ( ) ( V1() V4( the carrier of (b1 : ( ( ) ( ) RelStr ) [*] b2 : ( ( ) ( ) RelStr ) ) : ( ( strict ) ( strict ) RelStr ) : ( ( ) ( ) set ) ) V5( the carrier of (b1 : ( ( ) ( ) RelStr ) [*] b2 : ( ( ) ( ) RelStr ) ) : ( ( strict ) ( strict ) RelStr ) : ( ( ) ( ) set ) ) ) Element of K19(K20( the carrier of (b1 : ( ( ) ( ) RelStr ) [*] b2 : ( ( ) ( ) RelStr ) ) : ( ( strict ) ( strict ) RelStr ) : ( ( ) ( ) set ) , the carrier of (b1 : ( ( ) ( ) RelStr ) [*] b2 : ( ( ) ( ) RelStr ) ) : ( ( strict ) ( strict ) RelStr ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) & b : ( ( ) ( ) set ) in the carrier of R : ( ( ) ( ) RelStr ) : ( ( ) ( ) set ) holds
a : ( ( ) ( ) set ) in the carrier of R : ( ( ) ( ) RelStr ) : ( ( ) ( ) set ) ;

theorem :: LATSUM_1:22
for x, y being ( ( ) ( ) set )
for R, S being ( ( ) ( ) RelStr ) st [x : ( ( ) ( ) set ) ,y : ( ( ) ( ) set ) ] : ( ( ) ( ) set ) in the InternalRel of (R : ( ( ) ( ) RelStr ) [*] S : ( ( ) ( ) RelStr ) ) : ( ( strict ) ( strict ) RelStr ) : ( ( ) ( V1() V4( the carrier of (b3 : ( ( ) ( ) RelStr ) [*] b4 : ( ( ) ( ) RelStr ) ) : ( ( strict ) ( strict ) RelStr ) : ( ( ) ( ) set ) ) V5( the carrier of (b3 : ( ( ) ( ) RelStr ) [*] b4 : ( ( ) ( ) RelStr ) ) : ( ( strict ) ( strict ) RelStr ) : ( ( ) ( ) set ) ) ) Element of K19(K20( the carrier of (b3 : ( ( ) ( ) RelStr ) [*] b4 : ( ( ) ( ) RelStr ) ) : ( ( strict ) ( strict ) RelStr ) : ( ( ) ( ) set ) , the carrier of (b3 : ( ( ) ( ) RelStr ) [*] b4 : ( ( ) ( ) RelStr ) ) : ( ( strict ) ( strict ) RelStr ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) & the carrier of R : ( ( ) ( ) RelStr ) : ( ( ) ( ) set ) /\ the carrier of S : ( ( ) ( ) RelStr ) : ( ( ) ( ) set ) : ( ( ) ( ) set ) is ( ( upper ) ( upper ) Subset of ) & not ( x : ( ( ) ( ) set ) in the carrier of R : ( ( ) ( ) RelStr ) : ( ( ) ( ) set ) & y : ( ( ) ( ) set ) in the carrier of R : ( ( ) ( ) RelStr ) : ( ( ) ( ) set ) ) & not ( x : ( ( ) ( ) set ) in the carrier of S : ( ( ) ( ) RelStr ) : ( ( ) ( ) set ) & y : ( ( ) ( ) set ) in the carrier of S : ( ( ) ( ) RelStr ) : ( ( ) ( ) set ) ) holds
( x : ( ( ) ( ) set ) in the carrier of R : ( ( ) ( ) RelStr ) : ( ( ) ( ) set ) \ the carrier of S : ( ( ) ( ) RelStr ) : ( ( ) ( ) set ) : ( ( ) ( ) Element of K19( the carrier of b3 : ( ( ) ( ) RelStr ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) & y : ( ( ) ( ) set ) in the carrier of S : ( ( ) ( ) RelStr ) : ( ( ) ( ) set ) \ the carrier of R : ( ( ) ( ) RelStr ) : ( ( ) ( ) set ) : ( ( ) ( ) Element of K19( the carrier of b4 : ( ( ) ( ) RelStr ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ;

theorem :: LATSUM_1:23
for R, S being ( ( ) ( ) RelStr )
for a, b being ( ( ) ( ) Element of ( ( ) ( ) set ) ) st the carrier of R : ( ( ) ( ) RelStr ) : ( ( ) ( ) set ) /\ the carrier of S : ( ( ) ( ) RelStr ) : ( ( ) ( ) set ) : ( ( ) ( ) set ) is ( ( lower ) ( lower ) Subset of ) & a : ( ( ) ( ) Element of ( ( ) ( ) set ) ) <= b : ( ( ) ( ) Element of ( ( ) ( ) set ) ) & b : ( ( ) ( ) Element of ( ( ) ( ) set ) ) in the carrier of R : ( ( ) ( ) RelStr ) : ( ( ) ( ) set ) holds
a : ( ( ) ( ) Element of ( ( ) ( ) set ) ) in the carrier of R : ( ( ) ( ) RelStr ) : ( ( ) ( ) set ) ;

theorem :: LATSUM_1:24
for R, S being ( ( ) ( ) RelStr ) st R : ( ( ) ( ) RelStr ) tolerates S : ( ( ) ( ) RelStr ) & the carrier of R : ( ( ) ( ) RelStr ) : ( ( ) ( ) set ) /\ the carrier of S : ( ( ) ( ) RelStr ) : ( ( ) ( ) set ) : ( ( ) ( ) set ) is ( ( upper ) ( upper ) Subset of ) & the carrier of R : ( ( ) ( ) RelStr ) : ( ( ) ( ) set ) /\ the carrier of S : ( ( ) ( ) RelStr ) : ( ( ) ( ) set ) : ( ( ) ( ) set ) is ( ( lower ) ( lower ) Subset of ) & R : ( ( ) ( ) RelStr ) is transitive & R : ( ( ) ( ) RelStr ) is antisymmetric & S : ( ( ) ( ) RelStr ) is transitive & S : ( ( ) ( ) RelStr ) is antisymmetric holds
R : ( ( ) ( ) RelStr ) [*] S : ( ( ) ( ) RelStr ) : ( ( strict ) ( strict ) RelStr ) is antisymmetric ;

theorem :: LATSUM_1:25
for R, S being ( ( ) ( ) RelStr ) st the carrier of R : ( ( ) ( ) RelStr ) : ( ( ) ( ) set ) /\ the carrier of S : ( ( ) ( ) RelStr ) : ( ( ) ( ) set ) : ( ( ) ( ) set ) is ( ( upper ) ( upper ) Subset of ) & the carrier of R : ( ( ) ( ) RelStr ) : ( ( ) ( ) set ) /\ the carrier of S : ( ( ) ( ) RelStr ) : ( ( ) ( ) set ) : ( ( ) ( ) set ) is ( ( lower ) ( lower ) Subset of ) & R : ( ( ) ( ) RelStr ) tolerates S : ( ( ) ( ) RelStr ) & R : ( ( ) ( ) RelStr ) is transitive & S : ( ( ) ( ) RelStr ) is transitive holds
R : ( ( ) ( ) RelStr ) [*] S : ( ( ) ( ) RelStr ) : ( ( strict ) ( strict ) RelStr ) is transitive ;