begin
:: deftheorem defines one-to-one WAYBEL_1:def 1 :
:: deftheorem Def2 defines monotone WAYBEL_1:def 2 :
theorem
canceled;
theorem Th2:
theorem Th3:
theorem Th4:
theorem Th5:
:: deftheorem Def3 defines distributive WAYBEL_1:def 3 :
theorem Th6:
:: deftheorem defines ex_min_of WAYBEL_1:def 4 :
:: deftheorem Def5 defines ex_max_of WAYBEL_1:def 5 :
:: deftheorem Def6 defines is_minimum_of WAYBEL_1:def 6 :
:: deftheorem Def7 defines is_maximum_of WAYBEL_1:def 7 :
:: deftheorem Def8 defines are_isomorphic WAYBEL_1:def 8 :
theorem
theorem
begin
:: deftheorem Def9 defines Connection WAYBEL_1:def 9 :
:: deftheorem Def10 defines Galois WAYBEL_1:def 10 :
theorem Th9:
:: deftheorem Def11 defines upper_adjoint WAYBEL_1:def 11 :
:: deftheorem Def12 defines lower_adjoint WAYBEL_1:def 12 :
theorem Th10:
theorem Th11:
theorem Th12:
theorem Th13:
theorem Th14:
theorem Th15:
theorem Th16:
theorem
theorem Th18:
theorem Th19:
theorem Th20:
theorem Th21:
theorem Th22:
theorem Th23:
theorem Th24:
theorem Th25:
theorem
theorem Th27:
theorem Th28:
theorem
:: deftheorem Def13 defines projection WAYBEL_1:def 13 :
:: deftheorem Def14 defines closure WAYBEL_1:def 14 :
Lm1:
for L1, L2 being non empty RelStr
for f being Function of L1,L2 st L2 is reflexive holds
f <= f
:: deftheorem Def15 defines kernel WAYBEL_1:def 15 :
Lm2:
for L being non empty 1-sorted
for p being Function of L,L st p is idempotent holds
for x being set st x in rng p holds
p . x = x
theorem Th30:
theorem Th31:
:: deftheorem defines corestr WAYBEL_1:def 16 :
theorem Th32:
Lm3:
for L1, L2 being non empty RelStr
for g being Function of L1,L2 holds corestr g is onto
theorem Th33:
:: deftheorem defines inclusion WAYBEL_1:def 17 :
Lm4:
for L1, L2 being non empty RelStr
for g being Function of L1,L2 holds inclusion g is monotone
theorem
canceled;
theorem Th35:
theorem Th36:
theorem
theorem
theorem Th39:
theorem
theorem Th41:
theorem Th42:
theorem
theorem
theorem Th45:
theorem Th46:
theorem Th47:
theorem Th48:
theorem
theorem Th50:
theorem
theorem Th52:
theorem Th53:
theorem
theorem
theorem Th56:
theorem
theorem
theorem
begin
theorem Th60:
theorem
:: deftheorem Def18 defines "/\" WAYBEL_1:def 18 :
theorem Th62:
theorem Th63:
theorem Th64:
theorem Th65:
theorem Th66:
theorem
theorem Th68:
:: deftheorem Def19 defines Heyting WAYBEL_1:def 19 :
:: deftheorem Def20 defines => WAYBEL_1:def 20 :
theorem Th69:
:: deftheorem defines => WAYBEL_1:def 21 :
theorem Th70:
theorem Th71:
theorem Th72:
theorem
theorem
theorem Th75:
theorem
theorem
Lm5:
for H being non empty RelStr st H is Heyting holds
for a, b being Element of H holds a "/\" (a => b) <= b
theorem Th78:
theorem
theorem Th80:
theorem Th81:
:: deftheorem defines 'not' WAYBEL_1:def 22 :
theorem
theorem Th83:
theorem
theorem Th85:
theorem
theorem
theorem
:: deftheorem Def23 defines is_a_complement_of WAYBEL_1:def 23 :
:: deftheorem Def24 defines complemented WAYBEL_1:def 24 :
Lm6:
for L being bounded LATTICE st L is distributive & L is complemented holds
for x being Element of L ex x9 being Element of L st
for y being Element of L holds
( (y "\/" x9) "/\" x <= y & y <= (y "/\" x) "\/" x9 )
Lm7:
for L being bounded LATTICE st ( for x being Element of L ex x9 being Element of L st
for y being Element of L holds
( (y "\/" x9) "/\" x <= y & y <= (y "/\" x) "\/" x9 ) ) holds
( L is Heyting & ( for x being Element of L holds 'not' ('not' x) = x ) )
theorem Th89:
theorem Th90:
:: deftheorem Def25 defines Boolean WAYBEL_1:def 25 :