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