let X be set ; :: thesis: for R being Relation of X holds meet (rho R) = R
let R be Relation of X; :: thesis: meet (rho R) = R
thus meet (rho R) c= R :: according to XBOOLE_0:def 10 :: thesis: R c= meet (rho R)
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in meet (rho R) or x in R )
assume A2: x in meet (rho R) ; :: thesis: x in R
R in rho R ;
hence x in R by A2, SETFAM_1:def 1; :: thesis: verum
end;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in R or x in meet (rho R) )
assume A3: x in R ; :: thesis: x in meet (rho R)
now :: thesis: for Y being set st Y in rho R holds
x in Y
let Y be set ; :: thesis: ( Y in rho R implies x in Y )
assume Y in rho R ; :: thesis: x in Y
then ex S being Relation of X st
( Y = S & R c= S ) ;
hence x in Y by A3; :: thesis: verum
end;
hence x in meet (rho R) by SETFAM_1:def 1; :: thesis: verum