let L be non empty reflexive RelStr ; :: thesis: for x being set holds
( x is Element of iff x is closure Function of L,L )
let x be set ; :: thesis: ( x is Element of iff x is closure Function of L,L )
( x is Element of implies x is Element of ) by YELLOW_0:59;
hence ( x is Element of iff x is closure Function of L,L ) by Def2, Th10; :: thesis: verum