let L be complete LATTICE; :: thesis: 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; :: thesis: 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; :: thesis: for a, b being Element of S st a = x & b = y & x << y holds
a << b
let a, b be Element of S; :: thesis: ( a = x & b = y & x << y implies a << b )
assume that
A1: ( a = x & b = y ) and
A2: 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 ) ; :: according to WAYBEL_3:def 1 :: thesis: a << b
let D be non empty directed Subset of S; :: according to WAYBEL_3:def 1 :: thesis: ( not b <= "\/" D,S or ex b₁ being Element of the carrier of S st
( b₁ in D & a <= b₁ ) )
assume A3: b <= sup D ; :: thesis: ex b₁ being Element of the carrier of S st
( b₁ in D & a <= b₁ )
reconsider E = D as non empty directed Subset of L by YELLOW_2:7;
A4: 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 A4, YELLOW_0:65;
then y <= sup E by A1, A3, YELLOW_0:60;
then consider e being Element of L such that
A5: ( e in E & x <= e ) by A2;
reconsider d = e as Element of S by A5;
take d ; :: thesis: ( d in D & a <= d )
thus ( d in D & a <= d ) by A1, A5, YELLOW_0:61; :: thesis: verum