let L be non empty reflexive antisymmetric up-complete RelStr ; ( 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
; 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; (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
; verum