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)

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

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

f .: (meet F) c= meet { (f .: X) where X is Subset of A : X in F }
by Th3;
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 )

end;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

hence
y in f .: (meet F)
by FUNCT_1:def 6; :: thesis: verum
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

end;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

hence
( x0 in dom f & x0 in meet F & y = f . x0 )
by A3, A5, SETFAM_1:def 1; :: thesis: verum
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;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

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