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