let X be set ; :: thesis: for B being non empty Subset-Family of X
for L being Subset of (BoolePoset X) st B = L holds
<.B.] = uparrow L
let B be non empty Subset-Family of X; :: thesis: for L being Subset of (BoolePoset X) st B = L holds
<.B.] = uparrow L
let L be Subset of (BoolePoset X); :: thesis: ( B = L implies <.B.] = uparrow L )
assume A1: B = L ; :: thesis: <.B.] = uparrow L

hereby :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis: uparrow L c= <.B.]

let x be object ; :: thesis: ( x in <.B.] implies x in uparrow L )
assume A2: x in <.B.] ; :: thesis: x in uparrow L
then reconsider x0 = x as Subset of X ;
consider b being Element of B such that
A3: b c= x0 by A2, def3;
reconsider b1 = b as Element of (BoolePoset X) by LATTICE3:def 1;
reconsider x1 = x0 as Element of (BoolePoset X) by LATTICE3:def 1;
( b1 <= x1 & b1 in L ) by A3, A1, YELLOW_1:2;
hence x in uparrow L by WAYBEL_0:def 16; :: thesis: verum

end;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in uparrow L or x in <.B.] )
assume A4B1: x in uparrow L ; :: thesis: x in <.B.]
then reconsider x0 = x as Element of (BoolePoset X) ;
consider y being Element of (BoolePoset X) such that
A5B2: y <= x0 and
A6B3: y in L by A4B1, WAYBEL_0:def 16;
A7B4: y c= x0 by A5B2, YELLOW_1:2;
x0 is Element of bool X by LATTICE3:def 1;
then reconsider x1 = x as Subset of X ;
x1 in <.B.] by A1, A6B3, A7B4, def3;
hence x in <.B.] ; :: thesis: verum