let H be non empty complete Poset; :: thesis: ( H is Heyting iff ( H is meet-continuous & H is distributive ) )
hereby :: thesis: ( H is meet-continuous & H is distributive implies H is Heyting )
assume A1: H is Heyting ; :: thesis: ( H is meet-continuous & H is distributive )
then for x being Element of H holds x "/\" is lower_adjoint ;
then for X being Subset of H
for x being Element of H holds x "/\" (sup X) = "\/" ( { (x "/\" y) where y is Element of H : y in X } ,H) by WAYBEL_1:64;
then ( H is up-complete & H is satisfying_MC ) by Th37;
hence H is meet-continuous ; :: thesis: H is distributive
thus H is distributive by A1; :: thesis: verum
end;
assume A2: ( H is meet-continuous & H is distributive ) ; :: thesis: H is Heyting
thus H is LATTICE ; :: according to WAYBEL_1:def 19 :: thesis: for b1 being Element of the carrier of H holds b1 "/\" is lower_adjoint
let a be Element of H; :: thesis: a "/\" is lower_adjoint
( ( for X being finite Subset of H holds a "/\" preserves_sup_of X ) & ( for X being non empty directed Subset of H holds a "/\" preserves_sup_of X ) ) by A2, Th17, WAYBEL_0:def 37;
then a "/\" is sups-preserving by WAYBEL_0:74;
hence a "/\" is lower_adjoint by WAYBEL_1:17; :: thesis: verum