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 8;
hence EqClass z,PA c= EqClass z,PB by A1, EQREL_1:def 8; :: thesis: verum