let L, R be RelStr ; :: thesis: for x, y being Element of (Sub L) st y = R holds

( x <= y iff x is SubRelStr of R )

let x, y be Element of (Sub L); :: thesis: ( y = R implies ( x <= y iff x is SubRelStr of R ) )

( x <= y iff ex R being RelStr st

( y = R & x is SubRelStr of R ) ) by Def2;

hence ( y = R implies ( x <= y iff x is SubRelStr of R ) ) ; :: thesis: verum

( x <= y iff x is SubRelStr of R )

let x, y be Element of (Sub L); :: thesis: ( y = R implies ( x <= y iff x is SubRelStr of R ) )

( x <= y iff ex R being RelStr st

( y = R & x is SubRelStr of R ) ) by Def2;

hence ( y = R implies ( x <= y iff x is SubRelStr of R ) ) ; :: thesis: verum