let L be non empty RelStr ; :: thesis: for x being object holds
( x is Element of (ClosureSystems L) iff x is strict closure System of L )
let x be object ; :: thesis: ( x is Element of (ClosureSystems L) iff x is strict closure System of L )
( x is Element of (ClosureSystems L) implies x is Element of (Sub L) ) by YELLOW_0:58;
then ( x is Element of (ClosureSystems L) implies x is strict SubRelStr of L ) by Def2;
hence ( x is Element of (ClosureSystems L) iff x is strict closure System of L ) by Def3; :: thesis: verum