:: deftheorem Def20 defines => WAYBEL_1:def 20 :
for H being non empty RelStr
for a being Element of H st H is Heyting holds
for b₃ being Function of H,H holds
( b₃ = a => iff [b₃,(a "/\")] is Galois );