let H be non empty RelStr ; :: thesis: ( H is Heyting implies for a, b being Element of H st Top H = a => b & Top H = b => a holds
a = b )
assume A1: H is Heyting ; :: thesis: for a, b being Element of H st Top H = a => b & Top H = b => a holds
a = b
then A2: H is LATTICE ;
let a, b be Element of H; :: thesis: ( Top H = a => b & Top H = b => a implies a = b )
assume Top H = a => b ; :: thesis: ( not Top H = b => a or a = b )
then A3: a <= b by A1, Th72;
assume Top H = b => a ; :: thesis: a = b
then b <= a by A1, Th72;
hence a = b by A2, A3, ORDERS_2:25; :: thesis: verum