reconsider L = RealSubLatt ((In (0,REAL)),(In (1,REAL))) as complete Lattice by Th20;
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 Th23; :: thesis: verum