let L be Lattice; :: thesis: for p being Element of L
for D being non empty Subset of L st p in D holds
<.p.) c= <.D.)
let p be Element of L; :: thesis: for D being non empty Subset of L st p in D holds
<.p.) c= <.D.)
let D be non empty Subset of L; :: thesis: ( p in D implies <.p.) c= <.D.) )
assume A1: p in D ; :: thesis: <.p.) c= <.D.)
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in <.p.) or x in <.D.) )
assume x in <.p.) ; :: thesis: x in <.D.)
then A2: ex q being Element of L st
( x = q & p [= q ) ;
D c= <.D.) by Def5;
hence x in <.D.) by A1, A2, Th9; :: thesis: verum