let X be set ; :: thesis: for Y being lower Subset of (BoolePoset X) holds
( Y is directed iff for x, y being set st x in Y & y in Y holds
x \/ y in Y )
let Y be lower Subset of (BoolePoset X); :: thesis: ( Y is directed iff for x, y being set st x in Y & y in Y holds
x \/ y in Y )
hereby :: thesis: ( ( for x, y being set st x in Y & y in Y holds
x \/ y in Y ) implies Y is directed )
assume A1: Y is directed ; :: thesis: for x, y being set st x in Y & y in Y holds
x \/ y in Y
let x, y be set ; :: thesis: ( x in Y & y in Y implies x \/ y in Y )
assume A2: ( x in Y & y in Y ) ; :: thesis: x \/ y in Y
then reconsider a = x, b = y as Element of (BoolePoset X) ;
a "\/" b in Y by A1, A2, WAYBEL_0:40;
hence x \/ y in Y by YELLOW_1:17; :: thesis: verum
end;
assume A3: for x, y being set st x in Y & y in Y holds
x \/ y in Y ; :: thesis: Y is directed
now :: thesis: for a, b being Element of (BoolePoset X) st a in Y & b in Y holds
a "\/" b in Y
let a, b be Element of (BoolePoset X); :: thesis: ( a in Y & b in Y implies a "\/" b in Y )
assume ( a in Y & b in Y ) ; :: thesis: a "\/" b in Y
then a \/ b in Y by A3;
hence a "\/" b in Y by YELLOW_1:17; :: thesis: verum
end;
hence Y is directed by WAYBEL_0:40; :: thesis: verum