reconsider L = RealSubLatt (0,1) as complete Lattice by Th21;
take L ; :: thesis: ex L9 being SubLattice of L st
( L9 is \/-inheriting & not L9 is /\-inheriting )
thus ex L9 being SubLattice of L st
( L9 is \/-inheriting & not L9 is /\-inheriting ) by Th22; :: thesis: verum