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 )

proof

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;

thus ( 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 ) ; :: thesis: verum