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;