let k be Element of NAT ; :: thesis: for a, b being Element of (SubstPoset (NAT,{k}))
for X being Subset of (SubstPoset (NAT,{k})) st a is_<=_than X & b is_<=_than X holds
a "\/" b is_<=_than X
let a, b be Element of (SubstPoset (NAT,{k})); :: thesis: for X being Subset of (SubstPoset (NAT,{k})) st a is_<=_than X & b is_<=_than X holds
a "\/" b is_<=_than X
let X be Subset of (SubstPoset (NAT,{k})); :: thesis: ( a is_<=_than X & b is_<=_than X implies a "\/" b is_<=_than X )
assume A1: ( a is_<=_than X & b is_<=_than X ) ; :: thesis: a "\/" b is_<=_than X
let c be Element of (SubstPoset (NAT,{k})); :: according to LATTICE3:def 8 :: thesis: ( not c in X or a "\/" b <= c )
assume c in X ; :: thesis: a "\/" b <= c
then ( a <= c & b <= c ) by A1;
hence a "\/" b <= c by YELLOW_5:9; :: thesis: verum