let L be non empty RelStr ; :: thesis: for S being non empty SubRelStr of L
for X being Subset of S
for a being Element of L
for x being Element of S st x = a holds
( ( x is_<=_than X implies a is_<=_than X ) & ( x is_>=_than X implies a is_>=_than X ) )
let S be non empty SubRelStr of L; :: thesis: for X being Subset of S
for a being Element of L
for x being Element of S st x = a holds
( ( x is_<=_than X implies a is_<=_than X ) & ( x is_>=_than X implies a is_>=_than X ) )
let X be Subset of S; :: thesis: for a being Element of L
for x being Element of S st x = a holds
( ( x is_<=_than X implies a is_<=_than X ) & ( x is_>=_than X implies a is_>=_than X ) )
let a be Element of L; :: thesis: for x being Element of S st x = a holds
( ( x is_<=_than X implies a is_<=_than X ) & ( x is_>=_than X implies a is_>=_than X ) )
let x be Element of S; :: thesis: ( x = a implies ( ( x is_<=_than X implies a is_<=_than X ) & ( x is_>=_than X implies a is_>=_than X ) ) )
assume A1: x = a ; :: thesis: ( ( x is_<=_than X implies a is_<=_than X ) & ( x is_>=_than X implies a is_>=_than X ) )

hereby :: thesis: ( x is_>=_than X implies a is_>=_than X )

assume A2: x is_<=_than X ; :: thesis: a is_<=_than X
thus a is_<=_than X :: thesis: verum

proof

let b be Element of L; :: according to LATTICE3:def 8 :: thesis: ( not b in X or a <= b )
assume A3: b in X ; :: thesis: a <= b
then reconsider y = b as Element of S ;
x <= y by A2, A3, LATTICE3:def 8;
hence a <= b by A1, Th60; :: thesis: verum

end;

end;

assume A4: x is_>=_than X ; :: thesis: a is_>=_than X
let b be Element of L; :: according to LATTICE3:def 9 :: thesis: ( not b in X or b <= a )
assume A5: b in X ; :: thesis: b <= a
then reconsider y = b as Element of S ;
x >= y by A4, A5, LATTICE3:def 9;
hence b <= a by A1, Th60; :: thesis: verum