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 }

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

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;

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;

now :: thesis: for Y being set st Y in { (R .: X) where X is Subset of A : X in F } holds
y 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;

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

end;

end;