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 ;
then A4: EqClass (x,PA) meets EqClass (z,PA) by ;
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 ;
then ( z in EqClass (z,PB) & z in Y ) by ;
then Y meets EqClass (z,PB) by XBOOLE_0:3;
then A10: Y = EqClass (z,PB) by ;
x in EqClass (z,PB) by ;
then A11: EqClass (x,PB) meets EqClass (z,PB) by ;
( z in EqClass (z,PA) & z in X ) by ;
then X meets EqClass (z,PA) by XBOOLE_0:3;
then X = EqClass (z,PA) by ;
then A12: X = EqClass (x,PA) by ;
x in (EqClass (x,PA)) /\ (EqClass (x,PB)) by ;
hence x in EqClass (z,(PA '/\' PB)) by ; :: 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 ; :: thesis: verum
end;
hence EqClass (z,(PA '/\' PB)) = (EqClass (z,PA)) /\ (EqClass (z,PB)) by ; :: thesis: verum