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 ;
consider X0 being Subset of A such that
A3: ( z = f .: X0 & X0 in F ) by A2;
A4: y in f .: X0 by ;
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 ;
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 ;
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 ; :: thesis: verum
end;
hence ( x0 in dom f & x0 in meet F & y = f . x0 ) by ; :: 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 ; :: thesis: verum