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

( 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

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 7 :: thesis: ( x in P & y in P implies ex z being Element of L st
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;( 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

( 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