begin
:: deftheorem Def1 defines upper WAYBEL32:def 1 :
:: deftheorem Def2 defines order_consistent WAYBEL32:def 2 :
theorem Th1:
theorem
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem Th7:
theorem
theorem Th9:
theorem Th10:
theorem Th11:
theorem Th12:
theorem Th13:
theorem Th14:
theorem Th15:
theorem
theorem
theorem Th18:
theorem
theorem
theorem Th21:
theorem
theorem Th23:
theorem
theorem Th25:
theorem
definition
let S be non
empty 1-sorted ;
let R be non
empty RelStr ;
let f be
Function of the
carrier of
R,the
carrier of
S;
func R *' f -> non
empty strict NetStr of
S means :
Def3:
(
RelStr(# the
carrier of
it,the
InternalRel of
it #)
= RelStr(# the
carrier of
R,the
InternalRel of
R #) & the
mapping of
it = f );
existence
ex b1 being non empty strict NetStr of S st
( RelStr(# the carrier of b1,the InternalRel of b1 #) = RelStr(# the carrier of R,the InternalRel of R #) & the mapping of b1 = f )
uniqueness
for b1, b2 being non empty strict NetStr of S st RelStr(# the carrier of b1,the InternalRel of b1 #) = RelStr(# the carrier of R,the InternalRel of R #) & the mapping of b1 = f & RelStr(# the carrier of b2,the InternalRel of b2 #) = RelStr(# the carrier of R,the InternalRel of R #) & the mapping of b2 = f holds
b1 = b2
;
end;
:: deftheorem Def3 defines *' WAYBEL32:def 3 :
:: deftheorem Def4 defines inf_net WAYBEL32:def 4 :
theorem
canceled;
theorem Th28:
theorem Th29:
theorem
theorem Th31:
theorem
theorem Th33:
theorem