let L be continuous LATTICE; :: thesis: for p being Element of L st p is pseudoprime holds
for A being non empty finite Subset of L st inf A << p holds
ex a being Element of L st
( a in A & a <= p )
let p be Element of L; :: thesis: ( p is pseudoprime implies for A being non empty finite Subset of L st inf A << p holds
ex a being Element of L st
( a in A & a <= p ) )
given P being prime Ideal of L such that A1: p = sup P ; :: according to WAYBEL_7:def 6 :: thesis: for A being non empty finite Subset of L st inf A << p holds
ex a being Element of L st
( a in A & a <= p )
let A be non empty finite Subset of L; :: thesis: ( inf A << p implies ex a being Element of L st
( a in A & a <= p ) )
assume inf A << p ; :: thesis: ex a being Element of L st
( a in A & a <= p )
then A2: inf A in waybelow p ;
waybelow p c= P by A1, WAYBEL_5:1;
then consider a being Element of L such that
A3: ( a in A & a in P ) by A2, Th12;
take a ; :: thesis: ( a in A & a <= p )
ex_sup_of P,L by WAYBEL_0:75;
then P is_<=_than p by A1, YELLOW_0:30;
hence ( a in A & a <= p ) by A3, LATTICE3:def 9; :: thesis: verum