let H be non empty RelStr ; :: thesis: ( H is Heyting & H is lower-bounded implies for a being Element of H holds 'not' a is_maximum_of { x where x is Element of H : a "/\" x = Bottom H } )
assume that
A1: H is Heyting and
A2: H is lower-bounded ; :: thesis: for a being Element of H holds 'not' a is_maximum_of { x where x is Element of H : a "/\" x = Bottom H }
let a be Element of H; :: thesis: 'not' a is_maximum_of { x where x is Element of H : a "/\" x = Bottom H }
A3: H is LATTICE by A1;
set X = { x where x is Element of H : a "/\" x = Bottom H } ;
set Y = { x where x is Element of H : a "/\" x <= Bottom H } ;
A4: { x where x is Element of H : a "/\" x = Bottom H } = { x where x is Element of H : a "/\" x <= Bottom H }

proof

hereby :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis: { x where x is Element of H : a "/\" x <= Bottom H } c= { x where x is Element of H : a "/\" x = Bottom H }

let y be set ; :: thesis: ( y in { x where x is Element of H : a "/\" x = Bottom H } implies y in { x where x is Element of H : a "/\" x <= Bottom H } )
assume y in { x where x is Element of H : a "/\" x = Bottom H } ; :: thesis: y in { x where x is Element of H : a "/\" x <= Bottom H }
then consider x being Element of H such that
A5: y = x and
A6: a "/\" x = Bottom H ;
a "/\" x <= Bottom H by A3, A6, ORDERS_2:24;
hence y in { x where x is Element of H : a "/\" x <= Bottom H } by A5; :: thesis: verum

end;

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in { x where x is Element of H : a "/\" x <= Bottom H } or y in { x where x is Element of H : a "/\" x = Bottom H } )
assume y in { x where x is Element of H : a "/\" x <= Bottom H } ; :: thesis: y in { x where x is Element of H : a "/\" x = Bottom H }
then consider x being Element of H such that
A7: y = x and
A8: a "/\" x <= Bottom H ;
Bottom H <= a "/\" x by A2, A3, YELLOW_0:44;
then Bottom H = a "/\" x by A3, A8, ORDERS_2:25;
hence y in { x where x is Element of H : a "/\" x = Bottom H } by A7; :: thesis: verum

end;

for x being Element of H holds x "/\" is lower_adjoint by A1, Def19;
then A9: ex_max_of { x where x is Element of H : a "/\" x = Bottom H } ,H by A3, A4, Th65;
hence ex_sup_of { x where x is Element of H : a "/\" x = Bottom H } ,H by Def5; :: according to WAYBEL_1:def 7 :: thesis: ( 'not' a = "\/" { x where x is Element of H : a "/\" x = Bottom H } ,H & "\/" { x where x is Element of H : a "/\" x = Bottom H } ,H in { x where x is Element of H : a "/\" x = Bottom H } )
A10: 'not' a is_>=_than { x where x is Element of H : a "/\" x = Bottom H }

proof

let b be Element of H; :: according to LATTICE3:def 9 :: thesis: ( not b in { x where x is Element of H : a "/\" x = Bottom H } or b <= 'not' a )
assume b in { x where x is Element of H : a "/\" x = Bottom H } ; :: thesis: b <= 'not' a
then consider x being Element of H such that
A11: x = b and
A12: a "/\" x <= Bottom H by A4;
thus 'not' a >= b by A1, A11, A12, Th70; :: thesis: verum

end;

now

let b be Element of H; :: thesis: ( b is_>=_than { x where x is Element of H : a "/\" x = Bottom H } implies 'not' a <= b )
assume A13: b is_>=_than { x where x is Element of H : a "/\" x = Bottom H } ; :: thesis: 'not' a <= b
a => (Bottom H) <= a => (Bottom H) by A3, ORDERS_2:24;
then a "/\" ('not' a) <= Bottom H by A1, Th70;
then 'not' a in { x where x is Element of H : a "/\" x = Bottom H } by A4;
hence 'not' a <= b by A13, LATTICE3:def 9; :: thesis: verum

end;

hence 'not' a = "\/" { x where x is Element of H : a "/\" x = Bottom H } ,H by A3, A10, YELLOW_0:30; :: thesis: "\/" { x where x is Element of H : a "/\" x = Bottom H } ,H in { x where x is Element of H : a "/\" x = Bottom H }
thus "\/" { x where x is Element of H : a "/\" x = Bottom H } ,H in { x where x is Element of H : a "/\" x = Bottom H } by A9, Def5; :: thesis: verum