let H be non empty RelStr ; :: thesis: ( H is Heyting implies for a, b being Element of H holds b <= a => b )
assume A1: H is Heyting ; :: thesis: for a, b being Element of H holds b <= a => b
let a, b be Element of H; :: thesis: b <= a => b
a "/\" b <= b by A1, YELLOW_0:23;
hence b <= a => b by A1, Th67; :: thesis: verum