let L be non empty RelStr ; :: thesis: for X being Subset of L holds downarrow X = { x where x is Element of L : ex y being Element of L st
( x <= y & y in X ) }
let X be Subset of L; :: thesis: downarrow X = { x where x is Element of L : ex y being Element of L st
( x <= y & y in X ) }
set Y = { x where x is Element of L : ex y being Element of L st
( x <= y & y in X ) } ;

hereby :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis: { x where x is Element of L : ex y being Element of L st
( x <= y & y in X ) } c= downarrow X

let x be object ; :: thesis: ( x in downarrow X implies x in { x where x is Element of L : ex y being Element of L st
( x <= y & y in X ) } )
assume A1: x in downarrow X ; :: thesis: x in { x where x is Element of L : ex y being Element of L st
( x <= y & y in X ) }
then reconsider y = x as Element of L ;
ex z being Element of L st
( z >= y & z in X ) by A1, Def15;
hence x in { x where x is Element of L : ex y being Element of L st
( x <= y & y in X ) } ; :: thesis: verum

end;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { x where x is Element of L : ex y being Element of L st
( x <= y & y in X ) } or x in downarrow X )
assume x in { x where x is Element of L : ex y being Element of L st
( x <= y & y in X ) } ; :: thesis: x in downarrow X
then ex a being Element of L st
( a = x & ex y being Element of L st
( a <= y & y in X ) ) ;
hence x in downarrow X by Def15; :: thesis: verum