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 }
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 } ;
A3: { 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 object ; :: 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
A4: y = x and
A5: a "/\" x = Bottom H ;
a "/\" x <= Bottom H by A1, A5, ORDERS_2:1;
hence y in { x where x is Element of H : a "/\" x <= Bottom H } by A4; :: thesis: verum
end;
let y be object ; :: 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
A6: y = x and
A7: a "/\" x <= Bottom H ;
Bottom H <= a "/\" x by A1, A2, YELLOW_0:44;
then Bottom H = a "/\" x by A1, A7, ORDERS_2:2;
hence y in { x where x is Element of H : a "/\" x = Bottom H } by A6; :: thesis: verum
end;
A8: now :: thesis: for b being Element of H st b is_>=_than { x where x is Element of H : a "/\" x = Bottom H } holds
'not' a <= b
a => (Bottom H) <= a => (Bottom H) by A1, ORDERS_2:1;
then a "/\" ('not' a) <= Bottom H by A1, Th67;
then A9: 'not' a in { x where x is Element of H : a "/\" x = Bottom H } by A3;
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 b is_>=_than { x where x is Element of H : a "/\" x = Bottom H } ; :: thesis: 'not' a <= b
hence 'not' a <= b by A9; :: thesis: verum
end;
A10: ex_max_of { x where x is Element of H : a "/\" x = Bottom H } ,H by A1, A3, Th62;
hence ex_sup_of { x where x is Element of H : a "/\" x = Bottom H } ,H ; :: 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 } )
'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 ex x being Element of H st
( x = b & a "/\" x <= Bottom H ) by A3;
hence b <= 'not' a by A1, Th67; :: thesis: verum
end;
hence 'not' a = "\/" ( { x where x is Element of H : a "/\" x = Bottom H } ,H) by A1, A8, 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 A10; :: thesis: verum