let P be non empty complete Poset; :: thesis: for V being non empty Subset of P holds uparrow (sup V) = meet { (uparrow u) where u is Element of P : u in V }
let V be non empty Subset of P; :: thesis: uparrow (sup V) = meet { (uparrow u) where u is Element of P : u in V }
set F = { (uparrow u) where u is Element of P : u in V } ;
consider u being set such that
A1: u in V by XBOOLE_0:def 1;
reconsider u = u as Element of P by A1;
A2: uparrow u in { (uparrow u) where u is Element of P : u in V } by A1;
{ (uparrow u) where u is Element of P : u in V } c= bool the carrier of P

proof

let X be set ; :: according to TARSKI:def 3 :: thesis: ( not X in { (uparrow u) where u is Element of P : u in V } or X in bool the carrier of P )
assume X in { (uparrow u) where u is Element of P : u in V } ; :: thesis: X in bool the carrier of P
then consider u being Element of P such that
A3: ( X = uparrow u & u in V ) ;
thus X in bool the carrier of P by A3; :: thesis: verum

end;

then reconsider F = { (uparrow u) where u is Element of P : u in V } as Subset-Family of P ;
reconsider F = F as Subset-Family of P ;

now

let x be set ; :: thesis: ( ( x in uparrow (sup V) implies x in meet F ) & ( x in meet F implies x in uparrow (sup V) ) )

hereby :: thesis: ( x in meet F implies x in uparrow (sup V) )

assume A4: x in uparrow (sup V) ; :: thesis: x in meet F
then reconsider d = x as Element of P ;
A5: d >= sup V by A4, WAYBEL_0:18;

now

let Y be set ; :: thesis: ( Y in F implies x in Y )
assume Y in F ; :: thesis: x in Y
then consider u being Element of P such that
A6: ( Y = uparrow u & u in V ) ;
sup V is_>=_than V by YELLOW_0:32;
then sup V >= u by A6, LATTICE3:def 9;
then d >= u by A5, ORDERS_2:26;
hence x in Y by A6, WAYBEL_0:18; :: thesis: verum

end;

hence x in meet F by A2, SETFAM_1:def 1; :: thesis: verum

end;

assume A7: x in meet F ; :: thesis: x in uparrow (sup V)
then reconsider d = x as Element of P ;

now

let b be Element of P; :: thesis: ( b in V implies d >= b )
assume b in V ; :: thesis: d >= b
then uparrow b in F ;
then d in uparrow b by A7, SETFAM_1:def 1;
hence d >= b by WAYBEL_0:18; :: thesis: verum

end;

then d is_>=_than V by LATTICE3:def 9;
then d >= sup V by YELLOW_0:32;
hence x in uparrow (sup V) by WAYBEL_0:18; :: thesis: verum

end;

hence uparrow (sup V) = meet { (uparrow u) where u is Element of P : u in V } by TARSKI:2; :: thesis: verum