let Y be non empty set ; :: thesis: for PA, PB being a_partition of Y holds

( PA '<' PB iff ERl PA c= ERl PB )

let PA, PB be a_partition of Y; :: thesis: ( PA '<' PB iff ERl PA c= ERl PB )

set RA = ERl PA;

set RB = ERl PB;

for x being set st x in PA holds

ex y being set st

( y in PB & x c= y )

( PA '<' PB iff ERl PA c= ERl PB )

let PA, PB be a_partition of Y; :: thesis: ( PA '<' PB iff ERl PA c= ERl PB )

set RA = ERl PA;

set RB = ERl PB;

hereby :: thesis: ( ERl PA c= ERl PB implies PA '<' PB )

assume A4:
ERl PA c= ERl PB
; :: thesis: PA '<' PBassume A1:
PA '<' PB
; :: thesis: ERl PA c= ERl PB

for x1, x2 being object st [x1,x2] in ERl PA holds

[x1,x2] in ERl PB

end;for x1, x2 being object st [x1,x2] in ERl PA holds

[x1,x2] in ERl PB

proof

hence
ERl PA c= ERl PB
; :: thesis: verum
let x1, x2 be object ; :: thesis: ( [x1,x2] in ERl PA implies [x1,x2] in ERl PB )

assume [x1,x2] in ERl PA ; :: thesis: [x1,x2] in ERl PB

then consider A being Subset of Y such that

A2: A in PA and

A3: ( x1 in A & x2 in A ) by Def6;

ex y being set st

( y in PB & A c= y ) by A1, A2, SETFAM_1:def 2;

hence [x1,x2] in ERl PB by A3, Def6; :: thesis: verum

end;assume [x1,x2] in ERl PA ; :: thesis: [x1,x2] in ERl PB

then consider A being Subset of Y such that

A2: A in PA and

A3: ( x1 in A & x2 in A ) by Def6;

ex y being set st

( y in PB & A c= y ) by A1, A2, SETFAM_1:def 2;

hence [x1,x2] in ERl PB by A3, Def6; :: thesis: verum

for x being set st x in PA holds

ex y being set st

( y in PB & x c= y )

proof

hence
PA '<' PB
by SETFAM_1:def 2; :: thesis: verum
let x be set ; :: thesis: ( x in PA implies ex y being set st

( y in PB & x c= y ) )

assume A5: x in PA ; :: thesis: ex y being set st

( y in PB & x c= y )

then A6: x <> {} by EQREL_1:def 4;

set x0 = the Element of x;

set y = { z where z is Element of Y : [ the Element of x,z] in ERl PB } ;

A7: x c= { z where z is Element of Y : [ the Element of x,z] in ERl PB }

[ the Element of x, the Element of x] in ERl PA by A5, A6, Def6;

then consider B being Subset of Y such that

A9: B in PB and

A10: the Element of x in B and

the Element of x in B by A4, Def6;

A11: { z where z is Element of Y : [ the Element of x,z] in ERl PB } c= B

hence ex y being set st

( y in PB & x c= y ) by A7, A9; :: thesis: verum

end;( y in PB & x c= y ) )

assume A5: x in PA ; :: thesis: ex y being set st

( y in PB & x c= y )

then A6: x <> {} by EQREL_1:def 4;

set x0 = the Element of x;

set y = { z where z is Element of Y : [ the Element of x,z] in ERl PB } ;

A7: x c= { z where z is Element of Y : [ the Element of x,z] in ERl PB }

proof

set x1 = the Element of x;
let x1 be object ; :: according to TARSKI:def 3 :: thesis: ( not x1 in x or x1 in { z where z is Element of Y : [ the Element of x,z] in ERl PB } )

assume A8: x1 in x ; :: thesis: x1 in { z where z is Element of Y : [ the Element of x,z] in ERl PB }

then [ the Element of x,x1] in ERl PA by A5, Def6;

hence x1 in { z where z is Element of Y : [ the Element of x,z] in ERl PB } by A4, A5, A8; :: thesis: verum

end;assume A8: x1 in x ; :: thesis: x1 in { z where z is Element of Y : [ the Element of x,z] in ERl PB }

then [ the Element of x,x1] in ERl PA by A5, Def6;

hence x1 in { z where z is Element of Y : [ the Element of x,z] in ERl PB } by A4, A5, A8; :: thesis: verum

[ the Element of x, the Element of x] in ERl PA by A5, A6, Def6;

then consider B being Subset of Y such that

A9: B in PB and

A10: the Element of x in B and

the Element of x in B by A4, Def6;

A11: { z where z is Element of Y : [ the Element of x,z] in ERl PB } c= B

proof

B c= { z where z is Element of Y : [ the Element of x,z] in ERl PB }
let x2 be object ; :: according to TARSKI:def 3 :: thesis: ( not x2 in { z where z is Element of Y : [ the Element of x,z] in ERl PB } or x2 in B )

assume x2 in { z where z is Element of Y : [ the Element of x,z] in ERl PB } ; :: thesis: x2 in B

then ex z being Element of Y st

( z = x2 & [ the Element of x,z] in ERl PB ) ;

then consider B2 being Subset of Y such that

A12: B2 in PB and

A13: the Element of x in B2 and

A14: x2 in B2 by Def6;

B2 meets B by A10, A13, XBOOLE_0:3;

hence x2 in B by A9, A12, A14, EQREL_1:def 4; :: thesis: verum

end;assume x2 in { z where z is Element of Y : [ the Element of x,z] in ERl PB } ; :: thesis: x2 in B

then ex z being Element of Y st

( z = x2 & [ the Element of x,z] in ERl PB ) ;

then consider B2 being Subset of Y such that

A12: B2 in PB and

A13: the Element of x in B2 and

A14: x2 in B2 by Def6;

B2 meets B by A10, A13, XBOOLE_0:3;

hence x2 in B by A9, A12, A14, EQREL_1:def 4; :: thesis: verum

proof

then
{ z where z is Element of Y : [ the Element of x,z] in ERl PB } = B
by A11, XBOOLE_0:def 10;
let x2 be object ; :: according to TARSKI:def 3 :: thesis: ( not x2 in B or x2 in { z where z is Element of Y : [ the Element of x,z] in ERl PB } )

assume A15: x2 in B ; :: thesis: x2 in { z where z is Element of Y : [ the Element of x,z] in ERl PB }

then [ the Element of x,x2] in ERl PB by A9, A10, Def6;

hence x2 in { z where z is Element of Y : [ the Element of x,z] in ERl PB } by A15; :: thesis: verum

end;assume A15: x2 in B ; :: thesis: x2 in { z where z is Element of Y : [ the Element of x,z] in ERl PB }

then [ the Element of x,x2] in ERl PB by A9, A10, Def6;

hence x2 in { z where z is Element of Y : [ the Element of x,z] in ERl PB } by A15; :: thesis: verum

hence ex y being set st

( y in PB & x c= y ) by A7, A9; :: thesis: verum