let L be non empty RelStr ; :: thesis: for R being RelStr

for x, y being Element of (ClosureSystems L) st y = R holds

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

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

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

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

reconsider a = x, b = y as Element of (Sub L) by YELLOW_0:58;

( x <= y iff a <= b ) by YELLOW_0:59, YELLOW_0:60;

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

for x, y being Element of (ClosureSystems L) st y = R holds

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

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

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

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

reconsider a = x, b = y as Element of (Sub L) by YELLOW_0:58;

( x <= y iff a <= b ) by YELLOW_0:59, YELLOW_0:60;

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