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 A1: PA '<' PB ; :: thesis: EqClass z,PA c= EqClass z,PB
A2: ( z in EqClass z,PA & EqClass z,PA in PA ) by EQREL_1:def 8;
ex b being set st
( b in PB & EqClass z,PA c= b ) by A1, SETFAM_1:def 2;
hence EqClass z,PA c= EqClass z,PB by A2, EQREL_1:def 8; :: thesis: verum