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 object such that
A1: u in V by XBOOLE_0:def 1;
A2: { (uparrow u) where u is Element of P : u in V } c= bool the carrier of P

proof

let X be object ; :: 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 ex u being Element of P st
( X = uparrow u & u in V ) ;
hence X in bool the carrier of P ; :: thesis: verum

end;

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

now :: thesis: for x being object holds
( ( x in uparrow (sup V) implies x in meet F ) & ( x in meet F implies x in uparrow (sup V) ) )

let x be object ; :: 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 :: thesis: for Y being set st Y in F holds
x in Y

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 and
A7: u in V ;
sup V is_>=_than V by YELLOW_0:32;
then sup V >= u by A7, LATTICE3:def 9;
then d >= u by A5, ORDERS_2:3;
hence x in Y by A6, WAYBEL_0:18; :: thesis: verum

end;

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

end;

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

now :: thesis: for b being Element of P st b in V holds
d >= b

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 A8, 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