let A be set ; :: thesis: for D being a_partition of A holds ERl D = EqRelOf (PreorderFromPartition D)
let D be a_partition of A; :: thesis: ERl D = EqRelOf (PreorderFromPartition D)
for x, y being Element of A st [x,y] in ERl D holds
[x,y] in EqRelOf (PreorderFromPartition D)
proof
let x, y be Element of A; :: thesis: ( [x,y] in ERl D implies [x,y] in EqRelOf (PreorderFromPartition D) )
assume A1: [x,y] in ERl D ; :: thesis: [x,y] in EqRelOf (PreorderFromPartition D)
then A2: [y,x] in ERl D by EQREL_1:6;
reconsider X = x, Y = y as Element of (PreorderFromPartition D) ;
( X <= Y & Y <= X ) by A1, A2, ORDERS_2:def 5;
hence [x,y] in EqRelOf (PreorderFromPartition D) by Def6; :: thesis: verum
end;
hence ERl D c= EqRelOf (PreorderFromPartition D) by RELSET_1:def 1; :: according to XBOOLE_0:def 10 :: thesis: EqRelOf (PreorderFromPartition D) c= ERl D
for x, y being Element of A st [x,y] in EqRelOf (PreorderFromPartition D) holds
[x,y] in ERl D
proof
let x, y be Element of A; :: thesis: ( [x,y] in EqRelOf (PreorderFromPartition D) implies [x,y] in ERl D )
assume A3: [x,y] in EqRelOf (PreorderFromPartition D) ; :: thesis: [x,y] in ERl D
reconsider X = x, Y = y as Element of (PreorderFromPartition D) ;
X <= Y by A3, Def6;
hence [x,y] in ERl D by ORDERS_2:def 5; :: thesis: verum
end;
hence EqRelOf (PreorderFromPartition D) c= ERl D by RELSET_1:def 1; :: thesis: verum