let S be Subset of T; :: thesis: ( S is lower implies S is property(S) )
assume A1: S is lower ; :: thesis: S is property(S)
let D be non empty directed Subset of T; :: according to WAYBEL11:def 3 :: thesis: ( not "\/" (D,T) in S 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 S ) ) ) )
assume A2: sup D in S ; :: 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 S ) ) )
consider y being Element of T such that
A3: y in D by SUBSET_1:4;
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 S ) ) )
thus y in D by A3; :: thesis: for b₁ being Element of the carrier of T holds
( not b₁ in D or not y <= b₁ or b₁ in S )
let x be Element of T; :: thesis: ( not x in D or not y <= x or x in S )
assume that
A4: x in D and
x >= y ; :: thesis: x in S
x <= sup D by A4, Th17;
hence x in S by A1, A2; :: thesis: verum