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