let T be LATTICE; :: thesis: [#] T is property(S)
let D be non empty directed Subset of T; :: according to WAYBEL11:def 3 :: thesis: ( not "\/" (D,T) in [#] T or ex b₁ being Element of the carrier of T st
( b₁ in D & ( for b₂ being Element of the carrier of T holds
( not b₂ in D or not b₁ <= b₂ or b₂ in [#] T ) ) ) )
assume sup D in [#] T ; :: thesis: ex b₁ being Element of the carrier of T st
( b₁ in D & ( for b₂ being Element of the carrier of T holds
( not b₂ in D or not b₁ <= b₂ or b₂ in [#] T ) ) )
set y = the Element of D;
reconsider y = the Element of D as Element of T ;
take y ; :: thesis: ( y in D & ( for b₁ being Element of the carrier of T holds
( not b₁ in D or not y <= b₁ or b₁ in [#] T ) ) )
thus ( y in D & ( for b₁ being Element of the carrier of T holds
( not b₁ in D or not y <= b₁ or b₁ in [#] T ) ) ) ; :: thesis: verum