:: LATSUM_1 semantic presentation

theorem Th1: :: LATSUM_1:1
for b1, b2, b3, b4 being set st b1 in b3 \/ b4 & b2 in b3 \/ b4 & not ( b1 in b3 \ b4 & b2 in b3 \ b4 ) & not ( b1 in b4 & b2 in b4 ) & not ( b1 in b3 \ b4 & b2 in b4 ) holds
( b1 in b4 & b2 in b3 \ b4 )
proof end;

definition
let c1, c2 be RelStr ;
pred c1 tolerates c2 means :Def1: :: LATSUM_1:def 1
for b1, b2 being set st b1 in the carrier of a1 /\ the carrier of a2 & b2 in the carrier of a1 /\ the carrier of a2 holds
( [b1,b2] in the InternalRel of a1 iff [b1,b2] in the InternalRel of a2 );
end;

:: deftheorem Def1 defines tolerates LATSUM_1:def 1 :
for b1, b2 being RelStr holds
( b1 tolerates b2 iff for b3, b4 being set st b3 in the carrier of b1 /\ the carrier of b2 & b4 in the carrier of b1 /\ the carrier of b2 holds
( [b3,b4] in the InternalRel of b1 iff [b3,b4] in the InternalRel of b2 ) );

definition
let c1, c2 be RelStr ;
func c1 [*] c2 -> strict RelStr means :Def2: :: LATSUM_1:def 2
( the carrier of a3 = the carrier of a1 \/ the carrier of a2 & the InternalRel of a3 = (the InternalRel of a1 \/ the InternalRel of a2) \/ (the InternalRel of a1 * the InternalRel of a2) );
existence
ex b1 being strict RelStr st
( the carrier of b1 = the carrier of c1 \/ the carrier of c2 & the InternalRel of b1 = (the InternalRel of c1 \/ the InternalRel of c2) \/ (the InternalRel of c1 * the InternalRel of c2) )
proof end;
uniqueness
for b1, b2 being strict RelStr st the carrier of b1 = the carrier of c1 \/ the carrier of c2 & the InternalRel of b1 = (the InternalRel of c1 \/ the InternalRel of c2) \/ (the InternalRel of c1 * the InternalRel of c2) & the carrier of b2 = the carrier of c1 \/ the carrier of c2 & the InternalRel of b2 = (the InternalRel of c1 \/ the InternalRel of c2) \/ (the InternalRel of c1 * the InternalRel of c2) holds
b1 = b2 ;
end;

:: deftheorem Def2 defines [*] LATSUM_1:def 2 :
for b1, b2 being RelStr
for b3 being strict RelStr holds
( b3 = b1 [*] b2 iff ( the carrier of b3 = the carrier of b1 \/ the carrier of b2 & the InternalRel of b3 = (the InternalRel of b1 \/ the InternalRel of b2) \/ (the InternalRel of b1 * the InternalRel of b2) ) );

registration
let c1 be RelStr ;
let c2 be non empty RelStr ;
cluster a1 [*] a2 -> non empty strict ;
coherence
not c1 [*] c2 is empty
proof end;
end;

registration
let c1 be non empty RelStr ;
let c2 be RelStr ;
cluster a1 [*] a2 -> non empty strict ;
coherence
not c1 [*] c2 is empty
proof end;
end;

theorem Th2: :: LATSUM_1:2
for b1, b2 being RelStr holds
( the InternalRel of b1 c= the InternalRel of (b1 [*] b2) & the InternalRel of b2 c= the InternalRel of (b1 [*] b2) )
proof end;

theorem Th3: :: LATSUM_1:3
for b1, b2 being RelStr st b1 is reflexive & b2 is reflexive holds
b1 [*] b2 is reflexive
proof end;

theorem Th4: :: LATSUM_1:4
for b1, b2 being RelStr
for b3, b4 being set st [b3,b4] in the InternalRel of (b1 [*] b2) & b3 in the carrier of b1 & b4 in the carrier of b1 & b1 tolerates b2 & b1 is transitive holds
[b3,b4] in the InternalRel of b1
proof end;

theorem Th5: :: LATSUM_1:5
for b1, b2 being RelStr
for b3, b4 being set st [b3,b4] in the InternalRel of (b1 [*] b2) & b3 in the carrier of b2 & b4 in the carrier of b2 & b1 tolerates b2 & b2 is transitive holds
[b3,b4] in the InternalRel of b2
proof end;

theorem Th6: :: LATSUM_1:6
for b1, b2 being RelStr
for b3, b4 being set holds
( ( [b3,b4] in the InternalRel of b1 implies [b3,b4] in the InternalRel of (b1 [*] b2) ) & ( [b3,b4] in the InternalRel of b2 implies [b3,b4] in the InternalRel of (b1 [*] b2) ) )
proof end;

theorem Th7: :: LATSUM_1:7
for b1, b2 being non empty RelStr
for b3 being Element of (b1 [*] b2) holds
( b3 in the carrier of b1 or b3 in the carrier of b2 \ the carrier of b1 )
proof end;

theorem Th8: :: LATSUM_1:8
for b1, b2 being non empty RelStr
for b3, b4 being Element of b1
for b5, b6 being Element of (b1 [*] b2) st b3 = b5 & b4 = b6 & b1 tolerates b2 & b1 is transitive holds
( b3 <= b4 iff b5 <= b6 )
proof end;

theorem Th9: :: LATSUM_1:9
for b1, b2 being non empty RelStr
for b3, b4 being Element of (b1 [*] b2)
for b5, b6 being Element of b2 st b3 = b5 & b4 = b6 & b1 tolerates b2 & b2 is transitive holds
( b3 <= b4 iff b5 <= b6 )
proof end;

theorem Th10: :: LATSUM_1:10
for b1, b2 being non empty reflexive transitive antisymmetric with_suprema RelStr
for b3 being set st b3 in the carrier of b1 holds
b3 is Element of (b1 [*] b2)
proof end;

theorem Th11: :: LATSUM_1:11
for b1, b2 being non empty reflexive transitive antisymmetric with_suprema RelStr
for b3 being set st b3 in the carrier of b2 holds
b3 is Element of (b1 [*] b2)
proof end;

theorem Th12: :: LATSUM_1:12
for b1, b2 being non empty RelStr
for b3 being set st b3 in the carrier of b1 /\ the carrier of b2 holds
b3 is Element of b1
proof end;

theorem Th13: :: LATSUM_1:13
for b1, b2 being non empty RelStr
for b3 being set st b3 in the carrier of b1 /\ the carrier of b2 holds
b3 is Element of b2
proof end;

theorem Th14: :: LATSUM_1:14
for b1, b2 being non empty reflexive transitive antisymmetric with_suprema RelStr
for b3, b4 being Element of (b1 [*] b2) st b3 in the carrier of b1 & b4 in the carrier of b2 & b1 tolerates b2 holds
( b3 <= b4 iff ex b5 being Element of (b1 [*] b2) st
( b5 in the carrier of b1 /\ the carrier of b2 & b3 <= b5 & b5 <= b4 ) )
proof end;

theorem Th15: :: LATSUM_1:15
for b1, b2 being non empty RelStr
for b3, b4 being Element of b1
for b5, b6 being Element of b2 st b3 = b5 & b4 = b6 & b1 tolerates b2 & b1 is transitive & b2 is transitive holds
( b3 <= b4 iff b5 <= b6 )
proof end;

theorem Th16: :: LATSUM_1:16
for b1 being non empty reflexive transitive antisymmetric with_suprema RelStr
for b2 being directed lower Subset of b1
for b3, b4 being Element of b1 st b3 in b2 & b4 in b2 holds
b3 "\/" b4 in b2
proof end;

theorem Th17: :: LATSUM_1:17
for b1, b2 being RelStr
for b3, b4 being set st the carrier of b1 /\ the carrier of b2 is upper Subset of b1 & [b3,b4] in the InternalRel of (b1 [*] b2) & b3 in the carrier of b2 holds
b4 in the carrier of b2
proof end;

theorem Th18: :: LATSUM_1:18
for b1, b2 being RelStr
for b3, b4 being Element of (b1 [*] b2) st the carrier of b1 /\ the carrier of b2 is upper Subset of b1 & b3 <= b4 & b3 in the carrier of b2 holds
b4 in the carrier of b2
proof end;

theorem Th19: :: LATSUM_1:19
for b1, b2 being non empty reflexive transitive antisymmetric with_suprema RelStr
for b3, b4 being Element of b1
for b5, b6 being Element of b2 st the carrier of b1 /\ the carrier of b2 is directed lower Subset of b2 & the carrier of b1 /\ the carrier of b2 is upper Subset of b1 & b1 tolerates b2 & b3 = b5 & b4 = b6 holds
b3 "\/" b4 = b5 "\/" b6
proof end;

theorem Th20: :: LATSUM_1:20
for b1, b2 being non empty reflexive transitive antisymmetric lower-bounded with_suprema RelStr st the carrier of b1 /\ the carrier of b2 is non empty directed lower Subset of b2 holds
Bottom b2 in the carrier of b1
proof end;

theorem Th21: :: LATSUM_1:21
for b1, b2 being RelStr
for b3, b4 being set st the carrier of b1 /\ the carrier of b2 is lower Subset of b2 & [b3,b4] in the InternalRel of (b1 [*] b2) & b4 in the carrier of b1 holds
b3 in the carrier of b1
proof end;

theorem Th22: :: LATSUM_1:22
for b1, b2 being set
for b3, b4 being RelStr st [b1,b2] in the InternalRel of (b3 [*] b4) & the carrier of b3 /\ the carrier of b4 is upper Subset of b3 & not ( b1 in the carrier of b3 & b2 in the carrier of b3 ) & not ( b1 in the carrier of b4 & b2 in the carrier of b4 ) holds
( b1 in the carrier of b3 \ the carrier of b4 & b2 in the carrier of b4 \ the carrier of b3 )
proof end;

theorem Th23: :: LATSUM_1:23
for b1, b2 being RelStr
for b3, b4 being Element of (b1 [*] b2) st the carrier of b1 /\ the carrier of b2 is lower Subset of b2 & b3 <= b4 & b4 in the carrier of b1 holds
b3 in the carrier of b1
proof end;

theorem Th24: :: LATSUM_1:24
for b1, b2 being RelStr st b1 tolerates b2 & the carrier of b1 /\ the carrier of b2 is upper Subset of b1 & the carrier of b1 /\ the carrier of b2 is lower Subset of b2 & b1 is transitive & b1 is antisymmetric & b2 is transitive & b2 is antisymmetric holds
b1 [*] b2 is antisymmetric
proof end;

theorem Th25: :: LATSUM_1:25
for b1, b2 being RelStr st the carrier of b1 /\ the carrier of b2 is upper Subset of b1 & the carrier of b1 /\ the carrier of b2 is lower Subset of b2 & b1 tolerates b2 & b1 is transitive & b2 is transitive holds
b1 [*] b2 is transitive
proof end;