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: ( sup D in S implies ex y being Element of T st
( y in D & ( for x being Element of T st x in D & x >= y holds
x in S ) ) )
assume A2: sup D in S ; :: thesis: ex y being Element of T st
( y in D & ( for x being Element of T st x in D & x >= y holds
x 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 x being Element of T st x in D & x >= y holds
x in S ) )
thus y in D by A3; :: thesis: for x being Element of T st x in D & x >= y holds
x in S
let x be Element of T; :: thesis: ( x in D & x >= y implies x in S )
assume that
A4: x in D and
x >= y ; :: thesis: x in S
x <= sup D by A4, YELLOW_2:22;
hence x in S by A1, A2; :: thesis: verum