let H be non empty RelStr ; :: thesis: ( H is Heyting implies for x, a, y being Element of H holds
( x >= a "/\" y iff a => x >= y ) )
assume A1: H is Heyting ; :: thesis: for x, a, y being Element of H holds
( x >= a "/\" y iff a => x >= y )
let x, a, y be Element of H; :: thesis: ( x >= a "/\" y iff a => x >= y )
[(a =>),(a "/\")] is Galois by A1, Def20;
then ( x >= (a "/\") . y iff (a =>) . x >= y ) by A1, Th8;
hence ( x >= a "/\" y iff a => x >= y ) by Def18; :: thesis: verum