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 )

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 )
;

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

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

end;A2: R9 is antisymmetric

proof

A3:
R9 is transitive
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;assume ( x <<= y & x >>= y ) ; :: thesis: x = y

then ( x <= y & x >= y ) by Th3;

hence x = y by XXREAL_0:1; :: thesis: verum

proof

R9 is reflexive
by Th3;
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;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

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