let T be non empty reflexive TopRelStr ; :: thesis: [#] T is property(S)
let D be non empty directed Subset of T; :: according to WAYBEL11:def 3 :: thesis: ( sup D in [#] T 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 [#] T ) ) )
assume sup D in [#] T ; :: 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 [#] T ) )
consider y being Element of T such that
A1: 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 [#] T ) )
thus y in D by A1; :: thesis: for x being Element of T st x in D & x >= y holds
x in [#] T
let x be Element of T; :: thesis: ( x in D & x >= y implies x in [#] T )
assume that
x in D and
x >= y ; :: thesis: x in [#] T
thus x in [#] T ; :: thesis: verum