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
let a, b be Element of H; :: thesis: ( Top H = a => b & Top H = b => a implies a = b )
assume A2: Top H = a => b ; :: thesis: ( not Top H = b => a or a = b )
assume Top H = b => a ; :: thesis: a = b
then A3: b <= a by A1, Th69;
a <= b by A1, A2, Th69;
hence a = b by A1, A3, ORDERS_2:2; :: thesis: verum