let Y be non empty set ; :: thesis: for x, z0, t being set
for PA, PC being a_partition of Y st PA '<' PC & x in PC & z0 in PA & t in x & t in z0 holds
z0 c= x
let x, z0, t be set ; :: thesis: for PA, PC being a_partition of Y st PA '<' PC & x in PC & z0 in PA & t in x & t in z0 holds
z0 c= x
let PA, PC be a_partition of Y; :: thesis: ( PA '<' PC & x in PC & z0 in PA & t in x & t in z0 implies z0 c= x )
assume A1: ( PA '<' PC & x in PC & z0 in PA & t in x & t in z0 ) ; :: thesis: z0 c= x
then consider b being set such that
A2: ( b in PC & z0 c= b ) by SETFAM_1:def 2;
( x = b or x misses b ) by A1, A2, EQREL_1:def 6;
hence z0 c= x by A1, A2, XBOOLE_0:3; :: thesis: verum