let L be non empty RelStr ; :: thesis: for x being object holds

( x is Element of (Subalgebras L) iff x is strict closure directed-sups-inheriting System of L )

let x be object ; :: thesis: ( x is Element of (Subalgebras L) iff x is strict closure directed-sups-inheriting System of L )

( x is Element of (ClosureSystems L) iff x is strict closure System of L ) by Th16;

hence ( x is Element of (Subalgebras L) iff x is strict closure directed-sups-inheriting System of L ) by Def7, YELLOW_0:58; :: thesis: verum

( x is Element of (Subalgebras L) iff x is strict closure directed-sups-inheriting System of L )

let x be object ; :: thesis: ( x is Element of (Subalgebras L) iff x is strict closure directed-sups-inheriting System of L )

( x is Element of (ClosureSystems L) iff x is strict closure System of L ) by Th16;

hence ( x is Element of (Subalgebras L) iff x is strict closure directed-sups-inheriting System of L ) by Def7, YELLOW_0:58; :: thesis: verum