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 set ; :: 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 8;
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 8;
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 8;
then ( z in EqClass z,PB & z in Y ) by EQREL_1:def 8, 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 6;
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 8, XBOOLE_0:def 4;
then X meets EqClass z,PA by XBOOLE_0:3;
then X = EqClass z,PA by A6, EQREL_1:def 6;
then A12: X = EqClass x,PA by A4, EQREL_1:50;
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:50; :: thesis: verum

end;

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

proof

let x be set ; :: 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