:: ORDERS_4 semantic presentation

definition
mode Chain -> RelStr means :Def1: :: ORDERS_4:def 1
( a1 is non empty connected Poset or a1 is empty );
existence
ex b1 being RelStr st
( b1 is non empty connected Poset or b1 is empty )
proof end;
end;

:: deftheorem Def1 defines Chain ORDERS_4:def 1 :
for b1 being RelStr holds
( b1 is Chain iff ( b1 is non empty connected Poset or b1 is empty ) );

registration
cluster empty -> reflexive transitive antisymmetric RelStr ;
coherence
for b1 being RelStr st b1 is empty holds
( b1 is reflexive & b1 is transitive & b1 is antisymmetric )
proof end;
end;

registration
cluster -> reflexive transitive antisymmetric Chain ;
coherence
for b1 being Chain holds
( b1 is reflexive & b1 is transitive & b1 is antisymmetric )
proof end;
end;

registration
cluster non empty reflexive transitive antisymmetric Chain ;
existence
not for b1 being Chain holds b1 is empty
proof end;
end;

registration
cluster non empty -> non empty reflexive transitive antisymmetric connected Chain ;
coherence
for b1 being non empty Chain holds b1 is connected by Def1;
end;

definition
let c1 be 1-sorted ;
attr a1 is countable means :Def2: :: ORDERS_4:def 2
the carrier of a1 is countable;
end;

:: deftheorem Def2 defines countable ORDERS_4:def 2 :
for b1 being 1-sorted holds
( b1 is countable iff the carrier of b1 is countable );

registration
cluster non empty reflexive transitive antisymmetric connected finite Chain ;
existence
ex b1 being Chain st
( b1 is finite & not b1 is empty )
proof end;
end;

registration
cluster reflexive transitive antisymmetric countable Chain ;
existence
ex b1 being Chain st b1 is countable
proof end;
end;

registration
let c1 be non empty connected RelStr ;
cluster non empty full -> non empty connected SubRelStr of a1;
correctness
coherence
for b1 being non empty SubRelStr of c1 st b1 is full holds
b1 is connected;
proof end;
end;

registration
let c1 be finite RelStr ;
cluster -> finite SubRelStr of a1;
correctness
coherence
for b1 being SubRelStr of c1 holds b1 is finite;
proof end;
end;

theorem Th1: :: ORDERS_4:1
for b1, b2 being Nat st b1 <= b2 holds
InclPoset b1 is full SubRelStr of InclPoset b2
proof end;

definition
let c1 be RelStr ;
let c2, c3 be set ;
pred c2,c3 form_upper_lower_partition_of c1 means :Def3: :: ORDERS_4:def 3
( a2 \/ a3 = the carrier of a1 & ( for b1, b2 being Element of a1 st b1 in a2 & b2 in a3 holds
b1 < b2 ) );
end;

:: deftheorem Def3 defines form_upper_lower_partition_of ORDERS_4:def 3 :
for b1 being RelStr
for b2, b3 being set holds
( b2,b3 form_upper_lower_partition_of b1 iff ( b2 \/ b3 = the carrier of b1 & ( for b4, b5 being Element of b1 st b4 in b2 & b5 in b3 holds
b4 < b5 ) ) );

theorem Th2: :: ORDERS_4:2
for b1 being RelStr
for b2, b3 being set st b2,b3 form_upper_lower_partition_of b1 holds
b2 misses b3
proof end;

theorem Th3: :: ORDERS_4:3
for b1 being non empty antisymmetric upper-bounded RelStr holds the carrier of b1 \ {(Top b1)},{(Top b1)} form_upper_lower_partition_of b1
proof end;

theorem Th4: :: ORDERS_4:4
for b1, b2 being RelStr
for b3 being Function of b1,b2 st b3 is isomorphic holds
( ( the carrier of b1 <> {} implies the carrier of b2 <> {} ) & ( the carrier of b2 <> {} implies the carrier of b1 <> {} ) & ( the carrier of b2 <> {} or the carrier of b1 = {} ) & ( the carrier of b1 = {} implies the carrier of b2 = {} ) & ( the carrier of b2 = {} implies the carrier of b1 = {} ) )
proof end;

theorem Th5: :: ORDERS_4:5
for b1, b2 being antisymmetric RelStr
for b3, b4 being Subset of b1 st b3,b4 form_upper_lower_partition_of b1 holds
for b5, b6 being Subset of b2 st b5,b6 form_upper_lower_partition_of b2 holds
for b7 being Function of (subrelstr b3),(subrelstr b5) st b7 is isomorphic holds
for b8 being Function of (subrelstr b4),(subrelstr b6) st b8 is isomorphic holds
ex b9 being Function of b1,b2 st
( b9 = b7 +* b8 & b9 is isomorphic )
proof end;

theorem Th6: :: ORDERS_4:6
for b1 being finite Chain
for b2 being Nat st Card the carrier of b1 = b2 holds
b1, InclPoset b2 are_isomorphic
proof end;