let L be non empty RelStr ; :: thesis: for S being non empty full SubRelStr of L
for X being set
for a being Element of L
for x being Element of S st x = a holds
( ( a is_<=_than X implies x is_<=_than X ) & ( a is_>=_than X implies x is_>=_than X ) )
let S be non empty full SubRelStr of L; :: thesis: for X being set
for a being Element of L
for x being Element of S st x = a holds
( ( a is_<=_than X implies x is_<=_than X ) & ( a is_>=_than X implies x is_>=_than X ) )
let X be set ; :: thesis: for a being Element of L
for x being Element of S st x = a holds
( ( a is_<=_than X implies x is_<=_than X ) & ( a is_>=_than X implies x is_>=_than X ) )
let a be Element of L; :: thesis: for x being Element of S st x = a holds
( ( a is_<=_than X implies x is_<=_than X ) & ( a is_>=_than X implies x is_>=_than X ) )
let x be Element of S; :: thesis: ( x = a implies ( ( a is_<=_than X implies x is_<=_than X ) & ( a is_>=_than X implies x is_>=_than X ) ) )
assume A1: x = a ; :: thesis: ( ( a is_<=_than X implies x is_<=_than X ) & ( a is_>=_than X implies x is_>=_than X ) )
hereby :: thesis: ( a is_>=_than X implies x is_>=_than X )
assume A2: a is_<=_than X ; :: thesis: x is_<=_than X
thus x is_<=_than X :: thesis: verum
proof
let y be Element of S; :: according to LATTICE3:def 8 :: thesis: ( not y in X or x <= y )
reconsider b = y as Element of L by Th58;
assume y in X ; :: thesis: x <= y
then a <= b by A2;
hence x <= y by A1, Th60; :: thesis: verum
end;
end;
assume A3: a is_>=_than X ; :: thesis: x is_>=_than X
let y be Element of S; :: according to LATTICE3:def 9 :: thesis: ( not y in X or y <= x )
reconsider b = y as Element of L by Th58;
assume y in X ; :: thesis: y <= x
then a >= b by A3;
hence y <= x by A1, Th60; :: thesis: verum