let Y be non empty set ; :: thesis: for z being Element of Y
for PA, PB being a_partition of Y holds EqClass (z,(PA '/\' PB)) = (EqClass (z,PA)) /\ (EqClass (z,PB))
let z be Element of Y; :: thesis: for PA, PB being a_partition of Y holds EqClass (z,(PA '/\' PB)) = (EqClass (z,PA)) /\ (EqClass (z,PB))
let PA, PB be a_partition of Y; :: thesis: EqClass (z,(PA '/\' PB)) = (EqClass (z,PA)) /\ (EqClass (z,PB))
A1: (EqClass (z,PA)) /\ (EqClass (z,PB)) c= EqClass (z,(PA '/\' PB))

proof

set Z = EqClass (z,(PA '/\' PB));
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (EqClass (z,PA)) /\ (EqClass (z,PB)) or x in EqClass (z,(PA '/\' PB)) )
assume A2: x in (EqClass (z,PA)) /\ (EqClass (z,PB)) ; :: thesis: x in EqClass (z,(PA '/\' PB))
then reconsider x = x as Element of Y ;
A3: x in EqClass (x,PA) by EQREL_1:def 6;
x in EqClass (z,PA) by A2, XBOOLE_0:def 4;
then A4: EqClass (x,PA) meets EqClass (z,PA) by A3, XBOOLE_0:3;
A5: x in EqClass (x,PB) by EQREL_1:def 6;
PA '/\' PB = (INTERSECTION (PA,PB)) \ {{}} by PARTIT1:def 4;
then EqClass (z,(PA '/\' PB)) in INTERSECTION (PA,PB) by XBOOLE_0:def 5;
then consider X, Y being set such that
A6: X in PA and
A7: Y in PB and
A8: EqClass (z,(PA '/\' PB)) = X /\ Y by SETFAM_1:def 5;
A9: z in X /\ Y by A8, EQREL_1:def 6;
then ( z in EqClass (z,PB) & z in Y ) by EQREL_1:def 6, XBOOLE_0:def 4;
then Y meets EqClass (z,PB) by XBOOLE_0:3;
then A10: Y = EqClass (z,PB) by A7, EQREL_1:def 4;
x in EqClass (z,PB) by A2, XBOOLE_0:def 4;
then A11: EqClass (x,PB) meets EqClass (z,PB) by A5, XBOOLE_0:3;
( z in EqClass (z,PA) & z in X ) by A9, EQREL_1:def 6, XBOOLE_0:def 4;
then X meets EqClass (z,PA) by XBOOLE_0:3;
then X = EqClass (z,PA) by A6, EQREL_1:def 4;
then A12: X = EqClass (x,PA) by A4, EQREL_1:41;
x in (EqClass (x,PA)) /\ (EqClass (x,PB)) by A3, A5, XBOOLE_0:def 4;
hence x in EqClass (z,(PA '/\' PB)) by A11, A8, A10, A12, EQREL_1:41; :: thesis: verum

end;

EqClass (z,(PA '/\' PB)) c= (EqClass (z,PA)) /\ (EqClass (z,PB))

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in EqClass (z,(PA '/\' PB)) or x in (EqClass (z,PA)) /\ (EqClass (z,PB)) )
A13: ( EqClass (z,(PA '/\' PB)) c= EqClass (z,PA) & EqClass (z,(PA '/\' PB)) c= EqClass (z,PB) ) by BVFUNC11:3;
assume x in EqClass (z,(PA '/\' PB)) ; :: thesis: x in (EqClass (z,PA)) /\ (EqClass (z,PB))
hence x in (EqClass (z,PA)) /\ (EqClass (z,PB)) by A13, XBOOLE_0:def 4; :: thesis: verum

end;

hence EqClass (z,(PA '/\' PB)) = (EqClass (z,PA)) /\ (EqClass (z,PB)) by A1, XBOOLE_0:def 10; :: thesis: verum