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

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