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 Th22; :: thesis: verum