the carrier of L c= the carrier of L ;
then reconsider P = the carrier of L as Subset of ;
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 ; :: according to KNASTER:def 8 :: thesis: ( x in P & y in P implies ex z being Element of st
( z in P & x [= z & y [= z & ( for z' being Element of st z' in P & x [= z' & y [= z' holds
z [= z' ) ) )
assume that
x in P and
y in P ; :: thesis: ex z being Element of st
( z in P & x [= z & y [= z & ( for z' being Element of st z' in P & x [= z' & y [= z' holds
z [= z' ) )
take z = x "\/" y; :: thesis: ( z in P & x [= z & y [= z & ( for z' being Element of st z' in P & x [= z' & y [= z' holds
z [= z' ) )
thus z in P ; :: thesis: ( x [= z & y [= z & ( for z' being Element of st z' in P & x [= z' & y [= z' holds
z [= z' ) )
thus ( x [= z & y [= z ) by LATTICES:22; :: thesis: for z' being Element of st z' in P & x [= z' & y [= z' holds
z [= z'
let z' be Element of ; :: thesis: ( z' in P & x [= z' & y [= z' implies z [= z' )
assume that
z' in P and
A1: ( x [= z' & y [= z' ) ; :: thesis: z [= z'
thus z [= z' by A1, BOOLEALG:11; :: thesis: verum

end;

let x, y be Element of ; :: according to KNASTER:def 9 :: thesis: ( x in P & y in P implies ex z being Element of st
( z in P & z [= x & z [= y & ( for z' being Element of st z' in P & z' [= x & z' [= y holds
z' [= z ) ) )
assume that
x in P and
y in P ; :: thesis: ex z being Element of st
( z in P & z [= x & z [= y & ( for z' being Element of st z' in P & z' [= x & z' [= y holds
z' [= z ) )
take z = x "/\" y; :: thesis: ( z in P & z [= x & z [= y & ( for z' being Element of st z' in P & z' [= x & z' [= y holds
z' [= z ) )
thus z in P ; :: thesis: ( z [= x & z [= y & ( for z' being Element of st z' in P & z' [= x & z' [= y holds
z' [= z ) )
thus ( z [= x & z [= y ) by LATTICES:23; :: thesis: for z' being Element of st z' in P & z' [= x & z' [= y holds
z' [= z
let z' be Element of ; :: thesis: ( z' in P & z' [= x & z' [= y implies z' [= z )
assume that
z' in P and
A2: ( z' [= x & z' [= y ) ; :: thesis: z' [= z
thus z' [= z by A2, BOOLEALG:12; :: thesis: verum