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
A2: 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 A3: [x1,x2] in ERl PA ; :: thesis: [x1,x2] in ERl PB
consider A being Subset of Y such that
A4: A in PA and
A5: ( x1 in A & x2 in A ) by A3, Def6;
A6: ex y being set st
( y in PB & A c= y ) by A1, A4, SETFAM_1:def 2;
thus [x1,x2] in ERl PB by A5, A6, Def6; :: thesis: verum

end;

thus ERl PA c= ERl PB by A2, RELAT_1:def 3; :: thesis: verum

end;

assume A7: ERl PA c= ERl PB ; :: thesis: PA '<' PB
A8: 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 )
A10: x <> {} by A9, 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 }
A13: [x0,x1] in ERl PA by A9, A12, Def6;
thus x1 in { z where z is Element of Y : [x0,z] in ERl PB } by A7, A9, A12, A13; :: thesis: verum

end;

consider x1 being Element of x;
A14: [x0,x1] in ERl PA by A9, A10, Def6;
consider B being Subset of Y such that
A15: B in PB and
A16: x0 in B and
x1 in B by A7, A14, 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 A18: x2 in { z where z is Element of Y : [x0,z] in ERl PB } ; :: thesis: x2 in B
A19: ex z being Element of Y st
( z = x2 & [x0,z] in ERl PB ) by A18;
consider B2 being Subset of Y such that
A20: B2 in PB and
A21: x0 in B2 and
A22: x2 in B2 by A19, Def6;
A23: B2 meets B by A16, A21, XBOOLE_0:3;
thus x2 in B by A15, A20, A22, A23, EQREL_1:def 6; :: thesis: verum

end;

A24: 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 }
A26: [x0,x2] in ERl PB by A15, A16, A25, Def6;
thus x2 in { z where z is Element of Y : [x0,z] in ERl PB } by A25, A26; :: thesis: verum

end;

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

end;

thus PA '<' PB by A8, SETFAM_1:def 2; :: thesis: verum