let A be set ; :: thesis: for D being a_partition of A holds EqRelOf D = EqRelOf (PreorderFromPartition D)

let D be a_partition of A; :: thesis: EqRelOf D = EqRelOf (PreorderFromPartition D)

for x, y being Element of A st [x,y] in EqRelOf D holds

[x,y] in EqRelOf (PreorderFromPartition D)

for x, y being Element of A st [x,y] in EqRelOf (PreorderFromPartition D) holds

[x,y] in EqRelOf D

let D be a_partition of A; :: thesis: EqRelOf D = EqRelOf (PreorderFromPartition D)

for x, y being Element of A st [x,y] in EqRelOf D holds

[x,y] in EqRelOf (PreorderFromPartition D)

proof

hence
EqRelOf D c= EqRelOf (PreorderFromPartition D)
by RELSET_1:def 1; :: according to XBOOLE_0:def 10 :: thesis: EqRelOf (PreorderFromPartition D) c= EqRelOf D
let x, y be Element of A; :: thesis: ( [x,y] in EqRelOf D implies [x,y] in EqRelOf (PreorderFromPartition D) )

assume A1: [x,y] in EqRelOf D ; :: thesis: [x,y] in EqRelOf (PreorderFromPartition D)

then A2: [y,x] in EqRelOf 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;assume A1: [x,y] in EqRelOf D ; :: thesis: [x,y] in EqRelOf (PreorderFromPartition D)

then A2: [y,x] in EqRelOf 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

for x, y being Element of A st [x,y] in EqRelOf (PreorderFromPartition D) holds

[x,y] in EqRelOf D

proof

hence
EqRelOf (PreorderFromPartition D) c= EqRelOf D
by RELSET_1:def 1; :: thesis: verum
let x, y be Element of A; :: thesis: ( [x,y] in EqRelOf (PreorderFromPartition D) implies [x,y] in EqRelOf D )

assume A3: [x,y] in EqRelOf (PreorderFromPartition D) ; :: thesis: [x,y] in EqRelOf D

reconsider X = x, Y = y as Element of (PreorderFromPartition D) ;

X <= Y by A3, Def6;

hence [x,y] in EqRelOf D by ORDERS_2:def 5; :: thesis: verum

end;assume A3: [x,y] in EqRelOf (PreorderFromPartition D) ; :: thesis: [x,y] in EqRelOf D

reconsider X = x, Y = y as Element of (PreorderFromPartition D) ;

X <= Y by A3, Def6;

hence [x,y] in EqRelOf D by ORDERS_2:def 5; :: thesis: verum