let X, Y, Z be set ; :: thesis: ( X in Y & X c= Z implies meet Y c= Z )
assume that
A1: X in Y and
A2: X c= Z ; :: thesis: meet Y c= Z
meet Y c= X by A1, Th4;
hence meet Y c= Z by A2, XBOOLE_1:1; :: thesis: verum