let A be non empty Poset; :: thesis: for f being Choice_Function of (BOOL the carrier of A)
for fC1, fC2 being Chain of f holds fC1 meets fC2
let f be Choice_Function of (BOOL the carrier of A); :: thesis: for fC1, fC2 being Chain of f holds fC1 meets fC2
let fC1, fC2 be Chain of f; :: thesis: fC1 meets fC2
( f . the carrier of A in fC1 & f . the carrier of A in fC2 ) by Th37;
hence fC1 meets fC2 by XBOOLE_0:3; :: thesis: verum