let H be non empty complete Poset; :: thesis: ( H is Heyting iff ( H is meet-continuous & H is distributive ) )

thus H is LATTICE ; :: according to WAYBEL_1:def 19 :: thesis: for b_{1} being Element of the carrier of H holds b_{1} "/\" 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

hereby :: thesis: ( H is meet-continuous & H is distributive implies H is Heyting )

assume A2:
( H is meet-continuous & H is distributive )
; :: thesis: 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;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

thus H is LATTICE ; :: according to WAYBEL_1:def 19 :: thesis: for b

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