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

assume A1: X c= Y ; :: thesis: X /\ Y = X

thus X /\ Y c= X by Th17; :: according to XBOOLE_0:def 10 :: thesis: X c= X /\ Y

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in X or x in X /\ Y )

assume A2: x in X ; :: thesis: x in X /\ Y

then x in Y by A1;

hence x in X /\ Y by A2, XBOOLE_0:def 4; :: thesis: verum

assume A1: X c= Y ; :: thesis: X /\ Y = X

thus X /\ Y c= X by Th17; :: according to XBOOLE_0:def 10 :: thesis: X c= X /\ Y

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in X or x in X /\ Y )

assume A2: x in X ; :: thesis: x in X /\ Y

then x in Y by A1;

hence x in X /\ Y by A2, XBOOLE_0:def 4; :: thesis: verum