let Y be non empty set ; :: thesis: for z being Element of Y
for PA, PB being a_partition of Y st PA '<' PB holds
EqClass (z,PA) c= EqClass (z,PB)
let z be Element of Y; :: thesis: for PA, PB being a_partition of Y st PA '<' PB holds
EqClass (z,PA) c= EqClass (z,PB)
let PA, PB be a_partition of Y; :: thesis: ( PA '<' PB implies EqClass (z,PA) c= EqClass (z,PB) )
assume PA '<' PB ; :: thesis: EqClass (z,PA) c= EqClass (z,PB)
then A1: ex b being set st
( b in PB & EqClass (z,PA) c= b ) by SETFAM_1:def 2;
z in EqClass (z,PA) by EQREL_1:def 6;
hence EqClass (z,PA) c= EqClass (z,PB) by A1, EQREL_1:def 6; :: thesis: verum