let R be RelStr ; :: thesis: ( R is real implies ( R is reflexive & R is antisymmetric & R is transitive ) )
assume A1: R is real ; :: thesis: ( R is reflexive & R is antisymmetric & R is transitive )

per cases ( R is empty or not R is empty ) ;

suppose R is empty ; :: thesis: ( R is reflexive & R is antisymmetric & R is transitive )

hence ( R is reflexive & R is antisymmetric & R is transitive ) ; :: thesis: verum

end;

suppose not R is empty ; :: thesis: ( R is reflexive & R is antisymmetric & R is transitive )

then reconsider R9 = R as non empty real RelStr by A1;
A2: R9 is antisymmetric

proof

let x, y be Element of R9; :: according to YELLOW_0:def 3 :: thesis: ( not x <<= y or not y <<= x or x = y )
assume ( x <<= y & x >>= y ) ; :: thesis: x = y
then ( x <= y & x >= y ) by Th3;
hence x = y by XXREAL_0:1; :: thesis: verum

end;

A3: R9 is transitive

proof

let x, y, z be Element of R9; :: according to YELLOW_0:def 2 :: thesis: ( not x <<= y or not y <<= z or x <<= z )
assume ( x <<= y & y <<= z ) ; :: thesis: x <<= z
then ( x <= y & y <= z ) by Th3;
then x <= z by XXREAL_0:2;
hence x <<= z by Th3; :: thesis: verum

end;

R9 is reflexive by Th3;
hence ( R is reflexive & R is antisymmetric & R is transitive ) by A2, A3; :: thesis: verum

end;

end;