the carrier of L c= the carrier of L ;
then reconsider P = the carrier of L as Subset of L ;
take P ; :: thesis: ( not P is empty & P is with_suprema & P is with_infima )
thus not P is empty ; :: thesis: ( P is with_suprema & P is with_infima )
thus P is with_suprema :: thesis: P is with_infima
proof
let x, y be Element of L; :: according to KNASTER:def 6 :: thesis: ( x in P & y in P implies ex z being Element of L st
( z in P & x [= z & y [= z & ( for z9 being Element of L st z9 in P & x [= z9 & y [= z9 holds
z [= z9 ) ) )
assume that
x in P and
y in P ; :: thesis: ex z being Element of L st
( z in P & x [= z & y [= z & ( for z9 being Element of L st z9 in P & x [= z9 & y [= z9 holds
z [= z9 ) )
take z = x "\/" y; :: thesis: ( z in P & x [= z & y [= z & ( for z9 being Element of L st z9 in P & x [= z9 & y [= z9 holds
z [= z9 ) )
thus z in P ; :: thesis: ( x [= z & y [= z & ( for z9 being Element of L st z9 in P & x [= z9 & y [= z9 holds
z [= z9 ) )
thus ( x [= z & y [= z ) by LATTICES:5; :: thesis: for z9 being Element of L st z9 in P & x [= z9 & y [= z9 holds
z [= z9
let z9 be Element of L; :: thesis: ( z9 in P & x [= z9 & y [= z9 implies z [= z9 )
assume that
z9 in P and
A1: ( x [= z9 & y [= z9 ) ; :: thesis: z [= z9
thus z [= z9 by A1, BOOLEALG:5; :: thesis: verum
end;
let x, y be Element of L; :: according to KNASTER:def 7 :: thesis: ( x in P & y in P implies ex z being Element of L st
( z in P & z [= x & z [= y & ( for z9 being Element of L st z9 in P & z9 [= x & z9 [= y holds
z9 [= z ) ) )
assume that
x in P and
y in P ; :: thesis: ex z being Element of L st
( z in P & z [= x & z [= y & ( for z9 being Element of L st z9 in P & z9 [= x & z9 [= y holds
z9 [= z ) )
take z = x "/\" y; :: thesis: ( z in P & z [= x & z [= y & ( for z9 being Element of L st z9 in P & z9 [= x & z9 [= y holds
z9 [= z ) )
thus z in P ; :: thesis: ( z [= x & z [= y & ( for z9 being Element of L st z9 in P & z9 [= x & z9 [= y holds
z9 [= z ) )
thus ( z [= x & z [= y ) by LATTICES:6; :: thesis: for z9 being Element of L st z9 in P & z9 [= x & z9 [= y holds
z9 [= z
let z9 be Element of L; :: thesis: ( z9 in P & z9 [= x & z9 [= y implies z9 [= z )
assume that
z9 in P and
A2: ( z9 [= x & z9 [= y ) ; :: thesis: z9 [= z
thus z9 [= z by A2, BOOLEALG:6; :: thesis: verum