let A be set ; :: thesis: for F being Subset-Family of A

for R being Relation holds R .: (meet F) c= meet { (R .: X) where X is Subset of A : X in F }

let F be Subset-Family of A; :: thesis: for R being Relation holds R .: (meet F) c= meet { (R .: X) where X is Subset of A : X in F }

let R be Relation; :: thesis: R .: (meet F) c= meet { (R .: X) where X is Subset of A : X in F }

for R being Relation holds R .: (meet F) c= meet { (R .: X) where X is Subset of A : X in F }

let F be Subset-Family of A; :: thesis: for R being Relation holds R .: (meet F) c= meet { (R .: X) where X is Subset of A : X in F }

let R be Relation; :: thesis: R .: (meet F) c= meet { (R .: X) where X is Subset of A : X in F }

per cases
( meet F = {} or meet F <> {} )
;

end;

suppose
meet F = {}
; :: thesis: R .: (meet F) c= meet { (R .: X) where X is Subset of A : X in F }

then
R .: (meet F) = {}
;

hence R .: (meet F) c= meet { (R .: X) where X is Subset of A : X in F } by XBOOLE_1:2; :: thesis: verum

end;hence R .: (meet F) c= meet { (R .: X) where X is Subset of A : X in F } by XBOOLE_1:2; :: thesis: verum

suppose
meet F <> {}
; :: thesis: R .: (meet F) c= meet { (R .: X) where X is Subset of A : X in F }

then consider X0 being object such that

A1: X0 in F by SETFAM_1:1, XBOOLE_0:def 1;

reconsider X0 = X0 as Subset of A by A1;

A2: R .: X0 in { (R .: X) where X is Subset of A : X in F } by A1;

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in R .: (meet F) or y in meet { (R .: X) where X is Subset of A : X in F } )

assume y in R .: (meet F) ; :: thesis: y in meet { (R .: X) where X is Subset of A : X in F }

then consider x being object such that

A3: ( [x,y] in R & x in meet F ) by RELAT_1:def 13;

end;A1: X0 in F by SETFAM_1:1, XBOOLE_0:def 1;

reconsider X0 = X0 as Subset of A by A1;

A2: R .: X0 in { (R .: X) where X is Subset of A : X in F } by A1;

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in R .: (meet F) or y in meet { (R .: X) where X is Subset of A : X in F } )

assume y in R .: (meet F) ; :: thesis: y in meet { (R .: X) where X is Subset of A : X in F }

then consider x being object such that

A3: ( [x,y] in R & x in meet F ) by RELAT_1:def 13;

now :: thesis: for Y being set st Y in { (R .: X) where X is Subset of A : X in F } holds

y in Y

hence
y in meet { (R .: X) where X is Subset of A : X in F }
by A2, SETFAM_1:def 1; :: thesis: verumy in Y

let Y be set ; :: thesis: ( Y in { (R .: X) where X is Subset of A : X in F } implies y in Y )

assume Y in { (R .: X) where X is Subset of A : X in F } ; :: thesis: y in Y

then consider X being Subset of A such that

A4: ( Y = R .: X & X in F ) ;

x in X by A3, A4, SETFAM_1:def 1;

hence y in Y by A3, A4, RELAT_1:def 13; :: thesis: verum

end;assume Y in { (R .: X) where X is Subset of A : X in F } ; :: thesis: y in Y

then consider X being Subset of A such that

A4: ( Y = R .: X & X in F ) ;

x in X by A3, A4, SETFAM_1:def 1;

hence y in Y by A3, A4, RELAT_1:def 13; :: thesis: verum