let L be non empty reflexive RelStr ; :: thesis: for x being set holds
( x is Element of (DsupClOpers L) iff x is directed-sups-preserving closure Function of L,L )
let x be set ; :: thesis: ( x is Element of (DsupClOpers L) iff x is directed-sups-preserving closure Function of L,L )
( ( x is Element of (ClOpers L) implies x is closure Function of L,L ) & ( x is closure Function of L,L implies x is Element of (ClOpers L) ) & ( x is Element of (DsupClOpers L) implies x is Element of (ClOpers L) ) ) by Th11, YELLOW_0:59;
hence ( x is Element of (DsupClOpers L) iff x is directed-sups-preserving closure Function of L,L ) by Def7; :: thesis: verum