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 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 ) ; :: 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 A4: 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;
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 ; :: thesis: ( d in D & a <= d )
thus ( d in D & a <= d ) by A1, A6, A7, YELLOW_0:60; :: thesis: verum