let L be non empty RelStr ; :: thesis: ( L is reflexive & L is connected implies ( L is with_infima & L is with_suprema ) )

assume A1: ( L is reflexive & L is connected ) ; :: thesis: ( L is with_infima & L is with_suprema )

thus L is with_infima :: thesis: L is with_suprema_{1} being Element of the carrier of L st

( x <= b_{1} & y <= b_{1} & ( for b_{2} being Element of the carrier of L holds

( not x <= b_{2} or not y <= b_{2} or b_{1} <= b_{2} ) ) )

assume A1: ( L is reflexive & L is connected ) ; :: thesis: ( L is with_infima & L is with_suprema )

thus L is with_infima :: thesis: L is with_suprema

proof

let x, y be Element of L; :: according to LATTICE3:def 10 :: thesis: ex b
let x, y be Element of L; :: according to LATTICE3:def 11 :: thesis: ex b_{1} being Element of the carrier of L st

( b_{1} <= x & b_{1} <= y & ( for b_{2} being Element of the carrier of L holds

( not b_{2} <= x or not b_{2} <= y or b_{2} <= b_{1} ) ) )

end;( b

( not b

per cases
( x <= y or y <= x )
by A1;

end;

suppose A2:
x <= y
; :: thesis: ex b_{1} being Element of the carrier of L st

( b_{1} <= x & b_{1} <= y & ( for b_{2} being Element of the carrier of L holds

( not b_{2} <= x or not b_{2} <= y or b_{2} <= b_{1} ) ) )

( b

( not b

take z = x; :: thesis: ( z <= x & z <= y & ( for b_{1} being Element of the carrier of L holds

( not b_{1} <= x or not b_{1} <= y or b_{1} <= z ) ) )

thus ( z <= x & z <= y ) by A1, A2; :: thesis: for b_{1} being Element of the carrier of L holds

( not b_{1} <= x or not b_{1} <= y or b_{1} <= z )

thus for b_{1} being Element of the carrier of L holds

( not b_{1} <= x or not b_{1} <= y or b_{1} <= z )
; :: thesis: verum

end;( not b

thus ( z <= x & z <= y ) by A1, A2; :: thesis: for b

( not b

thus for b

( not b

suppose A3:
y <= x
; :: thesis: ex b_{1} being Element of the carrier of L st

( b_{1} <= x & b_{1} <= y & ( for b_{2} being Element of the carrier of L holds

( not b_{2} <= x or not b_{2} <= y or b_{2} <= b_{1} ) ) )

( b

( not b

take z = y; :: thesis: ( z <= x & z <= y & ( for b_{1} being Element of the carrier of L holds

( not b_{1} <= x or not b_{1} <= y or b_{1} <= z ) ) )

thus ( z <= x & z <= y ) by A1, A3; :: thesis: for b_{1} being Element of the carrier of L holds

( not b_{1} <= x or not b_{1} <= y or b_{1} <= z )

thus for b_{1} being Element of the carrier of L holds

( not b_{1} <= x or not b_{1} <= y or b_{1} <= z )
; :: thesis: verum

end;( not b

thus ( z <= x & z <= y ) by A1, A3; :: thesis: for b

( not b

thus for b

( not b

( x <= b

( not x <= b

per cases
( x <= y or y <= x )
by A1;

end;

suppose A4:
x <= y
; :: thesis: ex b_{1} being Element of the carrier of L st

( x <= b_{1} & y <= b_{1} & ( for b_{2} being Element of the carrier of L holds

( not x <= b_{2} or not y <= b_{2} or b_{1} <= b_{2} ) ) )

( x <= b

( not x <= b

take z = y; :: thesis: ( x <= z & y <= z & ( for b_{1} being Element of the carrier of L holds

( not x <= b_{1} or not y <= b_{1} or z <= b_{1} ) ) )

thus ( z >= x & z >= y ) by A1, A4; :: thesis: for b_{1} being Element of the carrier of L holds

( not x <= b_{1} or not y <= b_{1} or z <= b_{1} )

thus for b_{1} being Element of the carrier of L holds

( not x <= b_{1} or not y <= b_{1} or z <= b_{1} )
; :: thesis: verum

end;( not x <= b

thus ( z >= x & z >= y ) by A1, A4; :: thesis: for b

( not x <= b

thus for b

( not x <= b

suppose A5:
y <= x
; :: thesis: ex b_{1} being Element of the carrier of L st

( x <= b_{1} & y <= b_{1} & ( for b_{2} being Element of the carrier of L holds

( not x <= b_{2} or not y <= b_{2} or b_{1} <= b_{2} ) ) )

( x <= b

( not x <= b

take z = x; :: thesis: ( x <= z & y <= z & ( for b_{1} being Element of the carrier of L holds

( not x <= b_{1} or not y <= b_{1} or z <= b_{1} ) ) )

thus ( z >= x & z >= y ) by A1, A5; :: thesis: for b_{1} being Element of the carrier of L holds

( not x <= b_{1} or not y <= b_{1} or z <= b_{1} )

thus for b_{1} being Element of the carrier of L holds

( not x <= b_{1} or not y <= b_{1} or z <= b_{1} )
; :: thesis: verum

end;( not x <= b

thus ( z >= x & z >= y ) by A1, A5; :: thesis: for b

( not x <= b

thus for b

( not x <= b