let Y, Z be Element of rho R; :: thesis: ex T being Element of rho R st T c= Y /\ Z
Y in rho R ;
then consider SY being Subset of [:X,X:] such that
A1: Y = SY and
A2: R c= SY ;
Z in rho R ;
then consider SZ being Subset of [:X,X:] such that
A3: Z = SZ and
A4: R c= SZ ;
R in rho R ;
then reconsider T = R as Element of rho R ;
T c= Y /\ Z by A1, A3, A2, A4, XBOOLE_1:19;
hence ex T being Element of rho R st T c= Y /\ Z ; :: thesis: verum