begin
theorem Th1:
theorem
canceled;
theorem Th3:
theorem Th4:
theorem
theorem Th6:
theorem Th7:
theorem Th8:
theorem Th9:
begin
theorem Th10:
:: deftheorem WAYBEL10:def 1 :
canceled;
:: deftheorem Def2 defines ClOpers WAYBEL10:def 2 :
for L being non empty reflexive RelStr
for b2 being non empty strict full SubRelStr of MonMaps (L,L) holds
( b2 = ClOpers L iff for f being Function of L,L holds
( f is Element of b2 iff f is closure ) );
theorem Th11:
theorem Th12:
theorem Th13:
theorem Th14:
theorem Th15:
begin
:: deftheorem Def3 defines Sub WAYBEL10:def 3 :
for L being RelStr
for b2 being non empty strict RelStr holds
( b2 = Sub L iff ( ( for x being set holds
( x is Element of b2 iff x is strict SubRelStr of L ) ) & ( for a, b being Element of b2 holds
( a <= b iff ex R being RelStr st
( b = R & a is SubRelStr of R ) ) ) ) );
theorem Th16:
:: deftheorem Def4 defines ClosureSystems WAYBEL10:def 4 :
for L being non empty RelStr
for b2 being non empty strict full SubRelStr of Sub L holds
( b2 = ClosureSystems L iff for R being strict SubRelStr of L holds
( R is Element of b2 iff ( R is closure & R is full ) ) );
theorem Th17:
theorem Th18:
begin
:: deftheorem Def5 defines ClImageMap WAYBEL10:def 5 :
for L being non empty Poset
for b2 being Function of (ClOpers L),((ClosureSystems L) opp) holds
( b2 = ClImageMap L iff for c being closure Function of L,L holds b2 . c = Image c );
:: deftheorem Def6 defines closure_op WAYBEL10:def 6 :
for L being non empty RelStr
for S being SubRelStr of L
for b3 being Function of L,L holds
( b3 = closure_op S iff for x being Element of L holds b3 . x = "/\" (((uparrow x) /\ the carrier of S),L) );
theorem Th19:
theorem Th20:
theorem Th21:
theorem Th22:
theorem
begin
theorem Th24:
theorem Th25:
theorem
:: deftheorem Def7 defines DsupClOpers WAYBEL10:def 7 :
for L being non empty reflexive RelStr
for b2 being non empty strict full SubRelStr of ClOpers L holds
( b2 = DsupClOpers L iff for f being closure Function of L,L holds
( f is Element of b2 iff f is directed-sups-preserving ) );
theorem Th27:
:: deftheorem Def8 defines Subalgebras WAYBEL10:def 8 :
for L being non empty RelStr
for b2 being non empty strict full SubRelStr of ClosureSystems L holds
( b2 = Subalgebras L iff for R being strict closure System of L holds
( R is Element of b2 iff R is directed-sups-inheriting ) );
theorem Th28:
theorem Th29:
theorem