let L be RelStr ; :: thesis: for X, Y being set st X c= Y holds
for x being Element of L holds
( ( x is_<=_than Y implies x is_<=_than X ) & ( x is_>=_than Y implies x is_>=_than X ) )
let X, Y be set ; :: thesis: ( X c= Y implies for x being Element of L holds
( ( x is_<=_than Y implies x is_<=_than X ) & ( x is_>=_than Y implies x is_>=_than X ) ) )
assume A1: X c= Y ; :: thesis: for x being Element of L holds
( ( x is_<=_than Y implies x is_<=_than X ) & ( x is_>=_than Y implies x is_>=_than X ) )
let x be Element of L; :: thesis: ( ( x is_<=_than Y implies x is_<=_than X ) & ( x is_>=_than Y implies x is_>=_than X ) )
thus ( x is_<=_than Y implies x is_<=_than X ) :: thesis: ( x is_>=_than Y implies x is_>=_than X )

proof

assume A2: for y being Element of L st y in Y holds
y >= x ; :: according to LATTICE3:def 8 :: thesis: x is_<=_than X
let y be Element of L; :: according to LATTICE3:def 8 :: thesis: ( not y in X or x <= y )
thus ( not y in X or x <= y ) by A1, A2; :: thesis: verum

end;

assume A3: for y being Element of L st y in Y holds
y <= x ; :: according to LATTICE3:def 9 :: thesis: x is_>=_than X
let y be Element of L; :: according to LATTICE3:def 9 :: thesis: ( not y in X or y <= x )
thus ( not y in X or y <= x ) by A1, A3; :: thesis: verum