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