let P be non empty complete Poset; :: thesis: for V being non empty Subset of P holds downarrow (inf V) = meet { (downarrow u) where u is Element of P : u in V }
let V be non empty Subset of P; :: thesis: downarrow (inf V) = meet { (downarrow u) where u is Element of P : u in V }
set F = { (downarrow 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: { (downarrow 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 { (downarrow u) where u is Element of P : u in V } or X in bool the carrier of P )
assume X in { (downarrow 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 = downarrow 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: downarrow u in { (downarrow u) where u is Element of P : u in V } by A1;
reconsider F = { (downarrow 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 downarrow (inf V) implies x in meet F ) & ( x in meet F implies x in downarrow (inf V) ) )

let x be object ; :: thesis: ( ( x in downarrow (inf V) implies x in meet F ) & ( x in meet F implies x in downarrow (inf V) ) )

hereby :: thesis: ( x in meet F implies x in downarrow (inf V) )

assume A4: x in downarrow (inf V) ; :: thesis: x in meet F
then reconsider d = x as Element of P ;
A5: d <= inf V by A4, WAYBEL_0:17;

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 = downarrow u and
A7: u in V ;
inf V is_<=_than V by YELLOW_0:33;
then inf V <= u by A7, LATTICE3:def 8;
then d <= u by A5, ORDERS_2:3;
hence x in Y by A6, WAYBEL_0:17; :: 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 downarrow (inf 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 downarrow b in F ;
then d in downarrow b by A8, SETFAM_1:def 1;
hence d <= b by WAYBEL_0:17; :: thesis: verum

end;

then d is_<=_than V by LATTICE3:def 8;
then d <= inf V by YELLOW_0:33;
hence x in downarrow (inf V) by WAYBEL_0:17; :: thesis: verum

end;

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