let L be complete LATTICE; :: thesis: for S being non empty full sups-inheriting SubRelStr of L
for x, y being Element of
for a, b being Element of 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
for a, b being Element of st a = x & b = y & x << y holds
a << b
let x, y be Element of ; :: thesis: for a, b being Element of st a = x & b = y & x << y holds
a << b
let a, b be Element of ; :: 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 st y <= sup D holds
ex d being Element of st
( d in D & x <= d ) ; :: according to WAYBEL_3:def 1 :: thesis: a << b
let D be non empty directed Subset of ; :: 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 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:65;
then y <= sup E by A2, A4, YELLOW_0:60;
then consider e being Element of such that
A6: e in E and
A7: x <= e by A3;
reconsider d = e as Element of by A6;
take d ; :: thesis: ( d in D & a <= d )
thus ( d in D & a <= d ) by A1, A6, A7, YELLOW_0:61; :: thesis: verum