let L be complete LATTICE; for S being non empty full sups-inheriting SubRelStr of L
for x, y being Element of L
for a, b being Element of S st a = x & b = y & x << y holds
a << b
let S be non empty full sups-inheriting SubRelStr of L; for x, y being Element of L
for a, b being Element of S st a = x & b = y & x << y holds
a << b
let x, y be Element of L; for a, b being Element of S st a = x & b = y & x << y holds
a << b
let a, b be Element of S; ( a = x & b = y & x << y implies a << b )
assume that
A1:
a = x
and
A2:
b = y
and
A3:
for D being non empty directed Subset of L st y <= sup D holds
ex d being Element of L st
( d in D & x <= d )
; WAYBEL_3:def 1 a << b
let D be non empty directed Subset of S; WAYBEL_3:def 1 ( not b <= "\/" (D,S) or ex b1 being Element of the carrier of S st
( b1 in D & a <= b1 ) )
assume A4:
b <= sup D
; ex b1 being Element of the carrier of S st
( b1 in D & a <= b1 )
reconsider E = D as non empty directed Subset of L by YELLOW_2:7;
A5:
ex_sup_of D,L
by YELLOW_0:17;
then
"\/" (D,L) in the carrier of S
by YELLOW_0:def 19;
then
sup E = sup D
by A5, YELLOW_0:64;
then
y <= sup E
by A2, A4, YELLOW_0:59;
then consider e being Element of L such that
A6:
e in E
and
A7:
x <= e
by A3;
reconsider d = e as Element of S by A6;
take
d
; ( d in D & a <= d )
thus
( d in D & a <= d )
by A1, A6, A7, YELLOW_0:60; verum