let L be LATTICE; :: thesis: for x being Element of L holds

( x in Join-IRR L iff ( x <> Bottom L & ( for b, c being Element of L holds

( not x = b "\/" c or x = b or x = c ) ) ) )

let x be Element of L; :: thesis: ( x in Join-IRR L iff ( x <> Bottom L & ( for b, c being Element of L holds

( not x = b "\/" c or x = b or x = c ) ) ) )

thus ( x in Join-IRR L implies ( x <> Bottom L & ( for b, c being Element of L holds

( not x = b "\/" c or x = b or x = c ) ) ) ) :: thesis: ( x <> Bottom L & ( for b, c being Element of L holds

( not x = b "\/" c or x = b or x = c ) ) implies x in Join-IRR L )

( not x = b "\/" c or x = b or x = c ) ) implies x in Join-IRR L ) ; :: thesis: verum

( x in Join-IRR L iff ( x <> Bottom L & ( for b, c being Element of L holds

( not x = b "\/" c or x = b or x = c ) ) ) )

let x be Element of L; :: thesis: ( x in Join-IRR L iff ( x <> Bottom L & ( for b, c being Element of L holds

( not x = b "\/" c or x = b or x = c ) ) ) )

thus ( x in Join-IRR L implies ( x <> Bottom L & ( for b, c being Element of L holds

( not x = b "\/" c or x = b or x = c ) ) ) ) :: thesis: ( x <> Bottom L & ( for b, c being Element of L holds

( not x = b "\/" c or x = b or x = c ) ) implies x in Join-IRR L )

proof

thus
( x <> Bottom L & ( for b, c being Element of L holds
assume
x in Join-IRR L
; :: thesis: ( x <> Bottom L & ( for b, c being Element of L holds

( not x = b "\/" c or x = b or x = c ) ) )

then ex a being Element of L st

( x = a & a <> Bottom L & ( for b, c being Element of L holds

( not a = b "\/" c or a = b or a = c ) ) ) ;

hence ( x <> Bottom L & ( for b, c being Element of L holds

( not x = b "\/" c or x = b or x = c ) ) ) ; :: thesis: verum

end;( not x = b "\/" c or x = b or x = c ) ) )

then ex a being Element of L st

( x = a & a <> Bottom L & ( for b, c being Element of L holds

( not a = b "\/" c or a = b or a = c ) ) ) ;

hence ( x <> Bottom L & ( for b, c being Element of L holds

( not x = b "\/" c or x = b or x = c ) ) ) ; :: thesis: verum

( not x = b "\/" c or x = b or x = c ) ) implies x in Join-IRR L ) ; :: thesis: verum