let L be non empty RelStr ; :: thesis: for x being set holds
( x is Element of (Subalgebras L) iff x is strict closure directed-sups-inheriting System of L )
let x be set ; :: thesis: ( x is Element of (Subalgebras L) iff x is strict closure directed-sups-inheriting System of L )
( ( x is Element of (ClosureSystems L) implies x is strict closure System of L ) & ( x is strict closure System of L implies x is Element of (ClosureSystems L) ) & ( x is Element of (Subalgebras L) implies x is Element of (ClosureSystems L) ) ) by Th17, YELLOW_0:59;
hence ( x is Element of (Subalgebras L) iff x is strict closure directed-sups-inheriting System of L ) by Def8; :: thesis: verum