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 that
A1: PA '<' PC and
A2: x in PC and
A3: z0 in PA and
A4: ( t in x & t in z0 ) ; :: thesis: z0 c= x
consider b being set such that
A5: b in PC and
A6: z0 c= b by A1, A3, SETFAM_1:def 2;
( x = b or x misses b ) by A2, A5, EQREL_1:def 4;
hence z0 c= x by A4, A6, XBOOLE_0:3; :: thesis: verum