let X, Y, Z be set ; :: thesis: ( X meets Y & X c= Z implies X meets Y /\ Z )

assume that

A1: X meets Y and

A2: X c= Z ; :: thesis: X meets Y /\ Z

assume that

A1: X meets Y and

A2: X c= Z ; :: thesis: X meets Y /\ Z

now :: thesis: not X /\ (Y /\ Z) = {}

hence
X meets Y /\ Z
; :: thesis: verumassume A3:
X /\ (Y /\ Z) = {}
; :: thesis: contradiction

X /\ Y = (X /\ Z) /\ Y by A2, Th28

.= {} by A3, Th16 ;

hence contradiction by A1; :: thesis: verum

end;X /\ Y = (X /\ Z) /\ Y by A2, Th28

.= {} by A3, Th16 ;

hence contradiction by A1; :: thesis: verum