let A be set ; :: thesis: for F being Subset-Family of A
for f being one-to-one Function holds f .: (meet F) = meet { (f .: X) where X is Subset of A : X in F }
let F be Subset-Family of A; :: thesis: for f being one-to-one Function holds f .: (meet F) = meet { (f .: X) where X is Subset of A : X in F }
let f be one-to-one Function; :: thesis: f .: (meet F) = meet { (f .: X) where X is Subset of A : X in F }
set S = { (f .: X) where X is Subset of A : X in F } ;
A7: meet { (f .: X) where X is Subset of A : X in F } c= f .: (meet F)

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in meet { (f .: X) where X is Subset of A : X in F } or y in f .: (meet F) )
assume A1: y in meet { (f .: X) where X is Subset of A : X in F } ; :: thesis: y in f .: (meet F)
then consider z being object such that
A2: z in { (f .: X) where X is Subset of A : X in F } by XBOOLE_0:def 1, SETFAM_1:1;
consider X0 being Subset of A such that
A3: ( z = f .: X0 & X0 in F ) by A2;
A4: y in f .: X0 by A1, A2, A3, SETFAM_1:def 1;
ex x being object st
( x in dom f & x in meet F & y = f . x )

proof

consider x0 being object such that
A5: ( x0 in dom f & x0 in X0 & y = f . x0 ) by A4, FUNCT_1:def 6;
take x0 ; :: thesis: ( x0 in dom f & x0 in meet F & y = f . x0 )
for X being set st X in F holds
x0 in X

proof

let X be set ; :: thesis: ( X in F implies x0 in X )
assume X in F ; :: thesis: x0 in X
then f .: X in { (f .: X) where X is Subset of A : X in F } ;
then y in f .: X by A1, SETFAM_1:def 1;
then consider x being object such that
A6: ( x in dom f & x in X & y = f . x ) by FUNCT_1:def 6;
thus x0 in X by A5, A6, FUNCT_1:def 4; :: thesis: verum

end;

hence ( x0 in dom f & x0 in meet F & y = f . x0 ) by A3, A5, SETFAM_1:def 1; :: thesis: verum

end;

hence y in f .: (meet F) by FUNCT_1:def 6; :: thesis: verum

end;

f .: (meet F) c= meet { (f .: X) where X is Subset of A : X in F } by Th3;
hence f .: (meet F) = meet { (f .: X) where X is Subset of A : X in F } by A7, XBOOLE_0:def 10; :: thesis: verum