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
A1: p in S by SUBSET_1:4;
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 x in [#] L ; :: thesis: x in S
A2: x "/\" p in S by A1, Def22, Th4;
thus x in S by A2, Def23, Th4; :: thesis: verum
end;
hence S = [#] L by SUBSET_1:3; :: thesis: verum