let L be Lattice; :: thesis: for p being Element of L
for D being non empty Subset of L st D = {p} holds
<.D.) = <.p.)
let p be Element of L; :: thesis: for D being non empty Subset of L st D = {p} holds
<.D.) = <.p.)
let D be non empty Subset of L; :: thesis: ( D = {p} implies <.D.) = <.p.) )
assume A1: D = {p} ; :: thesis: <.D.) = <.p.)
D c= <.p.)

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in D or x in <.p.) )
assume x in D ; :: thesis: x in <.p.)
then x = p by A1, TARSKI:def 1;
hence x in <.p.) ; :: thesis: verum

end;

hence <.D.) c= <.p.) by Def4; :: according to XBOOLE_0:def 10 :: thesis: <.p.) c= <.D.)
p in D by A1, TARSKI:def 1;
hence <.p.) c= <.D.) by Th23; :: thesis: verum