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) iff x is closure Function of L,L ) by Th10;

hence ( x is Element of (DsupClOpers L) iff x is directed-sups-preserving closure Function of L,L ) by Def6, YELLOW_0:58; :: thesis: verum

( 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) iff x is closure Function of L,L ) by Th10;

hence ( x is Element of (DsupClOpers L) iff x is directed-sups-preserving closure Function of L,L ) by Def6, YELLOW_0:58; :: thesis: verum