let L be non empty reflexive antisymmetric up-complete RelStr ; :: thesis: ( inf_op L is directed-sups-preserving implies for D1, D2 being non empty directed Subset of L holds (sup D1) "/\" (sup D2) = sup (D1 "/\" D2) )

assume A1: inf_op L is directed-sups-preserving ; :: thesis: for D1, D2 being non empty directed Subset of L holds (sup D1) "/\" (sup D2) = sup (D1 "/\" D2)

let D1, D2 be non empty directed Subset of L; :: thesis: (sup D1) "/\" (sup D2) = sup (D1 "/\" D2)

set X = [:D1,D2:];

set f = inf_op L;

A2: inf_op L preserves_sup_of [:D1,D2:] by A1;

A3: ex_sup_of [:D1,D2:],[:L,L:] by WAYBEL_0:75;

A4: ( ex_sup_of D1,L & ex_sup_of D2,L ) by WAYBEL_0:75;

thus (sup D1) "/\" (sup D2) = (inf_op L) . ((sup D1),(sup D2)) by Def4

.= (inf_op L) . (sup [:D1,D2:]) by A4, YELLOW_3:43

.= sup ((inf_op L) .: [:D1,D2:]) by A2, A3

.= sup (D1 "/\" D2) by Th32 ; :: thesis: verum

assume A1: inf_op L is directed-sups-preserving ; :: thesis: for D1, D2 being non empty directed Subset of L holds (sup D1) "/\" (sup D2) = sup (D1 "/\" D2)

let D1, D2 be non empty directed Subset of L; :: thesis: (sup D1) "/\" (sup D2) = sup (D1 "/\" D2)

set X = [:D1,D2:];

set f = inf_op L;

A2: inf_op L preserves_sup_of [:D1,D2:] by A1;

A3: ex_sup_of [:D1,D2:],[:L,L:] by WAYBEL_0:75;

A4: ( ex_sup_of D1,L & ex_sup_of D2,L ) by WAYBEL_0:75;

thus (sup D1) "/\" (sup D2) = (inf_op L) . ((sup D1),(sup D2)) by Def4

.= (inf_op L) . (sup [:D1,D2:]) by A4, YELLOW_3:43

.= sup ((inf_op L) .: [:D1,D2:]) by A2, A3

.= sup (D1 "/\" D2) by Th32 ; :: thesis: verum