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
A2: ( A in PA & 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 A2, Def6; :: thesis: verum

end;

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

end;

assume A3: 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 A4: x in PA ; :: thesis: ex y being set st
( y in PB & x c= y )
then A5: 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 } ;
A6: 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 A7: 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 A4, Def6;
hence x1 in { z where z is Element of Y : [x0,z] in ERl PB } by A3, A4, A7; :: thesis: verum

end;

consider x1 being Element of x;
[x0,x1] in ERl PA by A4, A5, Def6;
then consider B being Subset of Y such that
A8: ( B in PB & x0 in B & x1 in B ) by A3, Def6;
{ z where z is Element of Y : [x0,z] in ERl PB } = B

proof

A9: { 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 consider z being Element of Y such that
A10: ( z = x2 & [x0,z] in ERl PB ) ;
consider B2 being Subset of Y such that
A11: ( B2 in PB & x0 in B2 & x2 in B2 ) by A10, Def6;
B2 meets B by A8, A11, XBOOLE_0:3;
hence x2 in B by A8, A11, 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 A12: 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 A8, Def6;
hence x2 in { z where z is Element of Y : [x0,z] in ERl PB } by A12; :: thesis: verum

end;

hence { z where z is Element of Y : [x0,z] in ERl PB } = B by A9, XBOOLE_0:def 10; :: thesis: verum

end;

hence ex y being set st
( y in PB & x c= y ) by A6, A8; :: thesis: verum

end;

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