set R = resource (X,A,f);
thus resource (X,A,f) is antisymmetric :: thesis: ( resource (X,A,f) is transitive & resource (X,A,f) is beta-transitive )

proof

let x be set ; :: according to MMLQUER2:def 2 :: thesis: for y being set st x,y in resource (X,A,f) & y,x in resource (X,A,f) holds
x = y
let y be set ; :: thesis: ( x,y in resource (X,A,f) & y,x in resource (X,A,f) implies x = y )
assume ( x,y in resource (X,A,f) & y,x in resource (X,A,f) ) ; :: thesis: x = y
then ( A <- (f . x) <> 0 & ( A <- (f . x) < A <- (f . y) or A <- (f . y) = 0 ) & A <- (f . y) <> 0 & ( A <- (f . y) < A <- (f . x) or A <- (f . x) = 0 ) ) by Def9;
hence x = y ; :: thesis: verum

end;

thus resource (X,A,f) is transitive :: thesis: resource (X,A,f) is beta-transitive

proof

let x be set ; :: according to MMLQUER2:def 1 :: thesis: for y, z being set st x,y in resource (X,A,f) & y,z in resource (X,A,f) holds
x,z in resource (X,A,f)
let y, z be set ; :: thesis: ( x,y in resource (X,A,f) & y,z in resource (X,A,f) implies x,z in resource (X,A,f) )
assume ( x,y in resource (X,A,f) & y,z in resource (X,A,f) ) ; :: thesis: x,z in resource (X,A,f)
then A1: ( x in X & y in X & A <- (f . x) <> 0 & ( A <- (f . x) < A <- (f . y) or A <- (f . y) = 0 ) & z in X & A <- (f . y) <> 0 & ( A <- (f . y) < A <- (f . z) or A <- (f . z) = 0 ) ) by Def9;
then ( A <- (f . x) < A <- (f . z) or A <- (f . z) = 0 ) by XXREAL_0:2;
hence x,z in resource (X,A,f) by A1, Def9; :: thesis: verum

end;

let x, y be Element of X; :: according to MMLQUER2:def 4 :: thesis: ( x,y nin resource (X,A,f) implies for z being Element of X st x,z in resource (X,A,f) holds
y,z in resource (X,A,f) )
assume A2: x,y nin resource (X,A,f) ; :: thesis: for z being Element of X st x,z in resource (X,A,f) holds
y,z in resource (X,A,f)
let z be Element of X; :: thesis: ( x,z in resource (X,A,f) implies y,z in resource (X,A,f) )
assume x,z in resource (X,A,f) ; :: thesis: y,z in resource (X,A,f)
then A3: ( x in X & z in X & A <- (f . x) <> 0 & ( A <- (f . x) < A <- (f . z) or A <- (f . z) = 0 ) & ( not x in X or not y in X or not A <- (f . x) <> 0 or ( not A <- (f . x) < A <- (f . y) & not A <- (f . y) = 0 ) ) ) by A2, Def9;
then ( A <- (f . y) <> 0 & ( A <- (f . y) < A <- (f . z) or A <- (f . z) = 0 ) ) by XXREAL_0:2;
hence y,z in resource (X,A,f) by A3, Def9; :: thesis: verum