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 ;
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 ;
hence y in Y by ; :: thesis: verum
end;
hence y in meet { (R .: X) where X is Subset of A : X in F } by ; :: thesis: verum
end;
end;