let L be Lattice; :: thesis: for S being non empty initial final Subset of L holds S = [#] L
let S be non empty initial final Subset of L; :: thesis: S = [#] L
consider p being Element of L such that
W: p in S by SUBSET_1:10;
for x being Element of L holds
( x in S iff x in [#] L )

proof

let x be Element of L; :: thesis: ( x in S iff x in [#] L )
thus ( x in S implies x in [#] L ) ; :: thesis: ( x in [#] L implies x in S )
assume Z: x in [#] L ; :: thesis: x in S
x "/\" p [= p by Th23;
then A: x "/\" p in S by W, Z, Defx;
x "/\" p [= x by Th23;
hence x in S by A, Z, Defy; :: thesis: verum

end;

hence S = [#] L by SUBSET_1:8; :: thesis: verum