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;

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

assume A1: PA '<' PB ; :: thesis: ERl PA c= ERl PB
for x1, x2 being set st [x1,x2] in ERl PA holds
[x1,x2] in ERl PB

proof

let x1, x2 be set ; :: 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
A4: A in PA and
A5: ( x1 in A & x2 in A ) by Def6;
ex y being set st
( y in PB & A c= y ) by A1, A4, SETFAM_1:def 2;
hence [x1,x2] in ERl PB by A5, Def6; :: thesis: verum

end;

hence ERl PA c= ERl PB by RELAT_1:def 3; :: thesis: verum

end;

assume A7: ERl PA c= ERl PB ; :: thesis: PA '<' PB
for x being set st x in PA holds
ex y being set st
( y in PB & x c= y )

proof

let x be set ; :: thesis: ( x in PA implies ex y being set st
( y in PB & x c= y ) )
assume A9: x in PA ; :: thesis: ex y being set st
( y in PB & x c= y )
then A10: x <> {} by EQREL_1:def 6;
consider x0 being Element of x;
set y = { z where z is Element of Y : [x0,z] in ERl PB } ;
A11: x c= { z where z is Element of Y : [x0,z] in ERl PB }

proof

let x1 be set ; :: according to TARSKI:def 3 :: thesis: ( not x1 in x or x1 in { z where z is Element of Y : [x0,z] in ERl PB } )
assume A12: x1 in x ; :: thesis: x1 in { z where z is Element of Y : [x0,z] in ERl PB }
then [x0,x1] in ERl PA by A9, Def6;
hence x1 in { z where z is Element of Y : [x0,z] in ERl PB } by A7, A9, A12; :: thesis: verum

end;

consider x1 being Element of x;
[x0,x1] in ERl PA by A9, A10, Def6;
then consider B being Subset of Y such that
A15: B in PB and
A16: x0 in B and
x1 in B by A7, Def6;
A17: { z where z is Element of Y : [x0,z] in ERl PB } c= B

proof

let x2 be set ; :: according to TARSKI:def 3 :: thesis: ( not x2 in { z where z is Element of Y : [x0,z] in ERl PB } or x2 in B )
assume x2 in { z where z is Element of Y : [x0,z] in ERl PB } ; :: thesis: x2 in B
then ex z being Element of Y st
( z = x2 & [x0,z] in ERl PB ) ;
then consider B2 being Subset of Y such that
A20: B2 in PB and
A21: x0 in B2 and
A22: x2 in B2 by Def6;
B2 meets B by A16, A21, XBOOLE_0:3;
hence x2 in B by A15, A20, A22, EQREL_1:def 6; :: thesis: verum

end;

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

proof

let x2 be set ; :: according to TARSKI:def 3 :: thesis: ( not x2 in B or x2 in { z where z is Element of Y : [x0,z] in ERl PB } )
assume A25: x2 in B ; :: thesis: x2 in { z where z is Element of Y : [x0,z] in ERl PB }
then [x0,x2] in ERl PB by A15, A16, Def6;
hence x2 in { z where z is Element of Y : [x0,z] in ERl PB } by A25; :: thesis: verum

end;

then { z where z is Element of Y : [x0,z] in ERl PB } = B by A17, XBOOLE_0:def 10;
hence ex y being set st
( y in PB & x c= y ) by A11, A15; :: thesis: verum

end;

hence PA '<' PB by SETFAM_1:def 2; :: thesis: verum